So this is a belated message about the Grace meetings in Lancaster. Early during the week (Tuesday evening) we held a BOF – mostly hosted by Kim – with a good group of people attending to hear about Grace. There were good discussions and questions, mostly about where we plan to go next. I wish I could have stayed for the whole thing!
Then on the Saturday, after the conference – while most people were heading home – Gary Leavens (University of Central Florida), Erik Ernst & Johan Winther (Aarhus Universitet), and Kim & James met for a “good, intense, and productive” time to talk over the next stages in the design – primarily the type system. Main choices so far include:
- A primarily gradual, parametric, structural type system
- Classes, Types, and Methods may all take generic parameters
- Generic types written as Array[T], following Eiffel and Ada.
- Constraints on type parameters expressed via where clauses, following CLU & C#
- Explicit union types e.g. (ListNode[T] | None) designed to work well with Grace’s pattern matching. These are inspired more directly by ML-style languages (& Ceylon) as an alternative to Scala’s case classes; although (as in general in Grace) they will remain primarily structural types
- No need for variance annotations — an ad-hoc structural interface can always be defined where necessary
- MyType and exact types at the top language level
Over the next few weeks – now we’re over the jetlag! – we hope to post on more details of this design, and eventually a 0.2 version of the language spec.
And although we’re just back from Lancaster, we also need to look forwards to the next time we’ll meet about Grace, which we’re planning at the SPLASH conference in Portland (Oregon) at the end of October. Our current thoughts are a general BOF early in the week (perhaps Monday evening) with a day-long design working session perhaps the Friday after the main conference ends.
We still have a little time to confirm these plans – if you’re thinking about going to SPLASH, we’d love to hear from you, so let us know when you’d be able to come along.
Are union types ML-style data definitions (implicitly tagged) or are they (non-disjoint) true union types. The latter will interact very badly with structural typing, I fear. The former looks like a good idea (I think having ML style data will work nicely with pattern matching).
Implicitly tagged is what we have in mind. I agree that set-style unions would be a disaster.
The current plan is for unions that are tagged, – but only in the sense that every object knows its own runtime type. Unions will not require an extra tag (as in ML).
This design follows Atsushi Igarashi’s design – below – modulo syntax (“|”) and underlying basis (structural rather than nominal). The main problem I can see with this is that structural pattern matching may not make important distinctions between objects: something like Modula-3 or Malayeri’s Unity’s brands here may help by reintroducing nominal typing where necessary.
If you can see other bad interactions with this design – please let us know!
————————————
Atsushi Igarashi, Hideshi Nagira: “Union Types for Object-Oriented Programming”, in Journal of Object Technology, vol. 6, no. 2, Special Issue OOPS Track at SAC 2006, February 2007, pages 47–68, http://www.jot.fm/issues/issues 2007_02/article3
Donna Malayeri and Jonathan Aldrich. Integrating nominal and structural subtyping. In Proceedings of ECOOP ’08, Paphos, Cyprus, July 2008.
James says “every object knows its own type”. Is that type nominal or structural? If the former, then fine, but then Grace uses nominal types. If the latter, then I fear the disaster that Kim mentions. I guess I need to read the Unity reference you gave. …[reading]… Unity looks nice but this would mean generally that brands would be in Grace — not just hidden in the Union types. I’m still unclear. If we have gradual typing then I don’t see how union types in the style of Igarashi and Nagira (i.e. tagless) can work unless there is nominal typing (every object knows its class). So, where am I now, I think union types are not going to work.
Either, TAG the unions (a la ML) OR unions may only use nominal types.
Structural untagged unions would be impossible to implement with gradual typing.
Structural untagged unions would be impossible to implement with gradual typing.
Impossible is, I think, a little strong. We can build ’em – we have got something going in prototypes anyway – but the problem from my perspective is that they will miss distinctions between objects – a variable node and a constant definition node in the Grace AST, say, would have exactly the same structural type. That’s certainly a problem waiting to happen, or rather, a whole pile of problems – I take it this is your & Kim’s disaster?
How do we address this? – brands is something we’re considering, although as you point out Unity brands are pretty much (nominal) classes. I guess we could permit brands as patterns in match statements, but not as types in variable or parameter declarations – but that asymmetry has its own problems. (I have an obscure ontological argument in favour of this: that types are not supposed to affect the execution of correct programs, so pattern matching shouldn’t use types!)
We could suggest (e.g. via lint) that programmers generally generally use only structural types by convention, but permit both nominal & structural types — except we don’t want conventions: we want positive rules.
We could optionally have programmers brand primarily structural types. For example if there variable node classes defines a method named “i_am_a_variable_node” the presumably that won’t match against constant nodes. This seems like the worst of all options – but perhaps it is an elegant resolution?
James, thanks for the response and the email. I think you put it very clearly that if types can be erased (gradual typing) then patterns can’t be types. One possibility is to let pattern matching be on classes, not types. Then we don’t need union types, since Igarashi union types are just a nice way to do structural typing. Unfortunately, the only way to have exhaustive pattern matching is to have an “Any” (aka “Object”) case, so it’s likely using pattern matching would mean “MatchError” would be a common way for programs to die.
Another possibility is to have ML datatypes with a fixed set of constructors. This is not OO, but allows Option types to be defined easily.
You mentioned Newspeak in your email; using methods to do pattern matching. That’s interesting.
What’s the consensus experience of how well it works?
if types can be erased (gradual typing) then patterns can’t be types
right – or “patterns” cannot be erased (even if some patterns are technically type)
Unfortunately, the only way to have exhaustive pattern matching is to have an Any…
Ah, but this is what I like about “Bruce’s device” — i.e. the Union types: when you match across a union, if you have a case for each summand, you can be sure you are exhaustive without needing an “Any” case.
I see ML datatypes as doing two things: each constructor declares a nominal type (like a vestigial class), and then the datatype as a whole is the union of those constructors. Grace has individual classes to define each “constructor” individually, and then unions to bind them together.
So while something like
is rather more verbose than
… its not that much worse.
You mentioned Newspeak in your email; … What’s the consensus experience of how well it works?
Gilad only knows!
James wrote: “the problem from my perspective is that they will miss distinctions between objects – a variable node and a constant definition node in the Grace AST, say, would have exactly the same structural type.”
I would ask: are they really the same? I would have expected, for example, that a variable would have a method to generate an assignment to that variable, whereas a constant would not. So, if the type are the same, the programmer should stop and think: are these really two different implementation of the SAME type, or are are they different types, and if so, what, abstractly, is the difference? If there really is a difference, then that should be reflected in the message suite.
One of the dangers of typecase is that it encourages programmers to write noon-OO code: asking what an object is and doing stuff to it, rather than telling the object to do something on its own behalf.
Andrew asks: are they really the same?
well the version of the minigrace compiler I looked at a couple of weeks ago, they certainly were the same. I don’t see why all these differences have to be reflected in the (public) message suite, as against in the behaviours provided by that suite. Certainly in a nominally typed language programmers can make this distinction – and ML-style tagged summand constructors count as nominal, as far as I’m concerned…
One of the dangers of typecase is that it encourages programmers to write non-OO code:
yes it does – but for both procedural and functional programming, people want to write non-OO code. I see Grace as an OO language, with “objects all the way down” but providing support for teaching other styles. Match/case is probably the key piece of that support.
Sorry, I still stuck on “every object knows its type”. Is this nominal or structural? If the former, then fine, we can do the kind of union we want. If the latter, then gradual typing is going to run into trouble (“Mark my words!”).
“every object knows its type”. Is this nominal or structural
Short answer – it’s the type of the object – like the reflexive type information kept about an object in C#. If the object is an instance of a generic class – and that class is instantiated with a structural type – then that’s what the type information about the object will be.
Grace’s types are primarily structural, except for the unions, which are nominal insofar as the only subtypes or A or B are subtypes of A | B – Andrew suggests we call these “untagged variants” – which seems good, since they’re not really structural unions.
I do “mark your works!” – but I’m afraid I still don’t see the problematic interaction between gradual typing, structural types, and these unions. Can you send an example?