Ownership and generics are both desirable in a language: (to paraphrase the OGJ paper) generics let you say I have a list of books (rather than just a list) and ownership types let you say this is my book (rather than just a book). It is also desirable to have both, that is, to say this is a list of my books; and both are needed - there is no overlap in expressivity.
There are basically two ways to combine generics and ownership: orthogonally, where both are present and fulfil their standard tasks without much overlap, and the mixed approach, where type parameters provide the ownership information. (My terminology, and I don't think it is very good terminology at that). Jo\exists, generic universes, and generic confinement fall into the first camp, OGJ, OIGJ, WOGJ, etc. fall into the second.
Example in the orthogonal style:
List<owner,X> {
List<owner,X> next;
X datum;
}
Example in the mixed style:
List<Owner,X> {
List<Owner,X> next;
X datum;
}
So, not much difference in this example, but the subtle difference is an important one: the first example has two kinds of parameter (context parameters and type parameters) and the second example only has type parameters - the type rules are tweaked slightly to enforce ownership.
My opinion is twofold: first that adding generics adds expressive power to an ownership language and second that the orthogonal way, with an adjustment, is the better way to do things, and furthermore, in this case you don't need context parameters at all (other than the owner).
So first off, the 'generics are good' bit: a non-generic list only lets you express the owner of the list and the owner of objects in the list. A generic list lets you express these things and other contexts relevant to objects in the list; for example, List<world,Button<>this,win>, I'm imagining a list of buttons where the buttons have fields owned by the window they're placed in. Without generics the best I could do is List<world,this>, I have to forget about the window the buttons are in (as well as the fact that they are buttons, obviously).
Second, the adjustment, in regular ownership types the owner and other context parameters are usually grouped together. However, if you look at the type rules they are often treated differently, or the owner is treated as a special case. This is made explicit in Joe_3 and some other calculi by putting the owner before the type and separating it from the other context parameters: eg, world:List<this> for a list owned by world containing objects owned by this.
My opinion is that the owner context should be treated differently to the other context parameters and should not be a type parameter. This is because I think that although the behaviour is similar (almost the same as) a context or type parameter it does something extra and different and that it is confusing to confuse the two concepts. This means that type parameters in my ideal system are all just type parameters, there is no special This or World types with special meaning.
Now what is nice is that with generics you no longer need context parameters: you can trivially replace any context parameter with a type parameter and the actual context parameter a, with the actual type parameter a:Object. However, I believe you don't really need to do even this, because any extra context parameters should be in some way tied to a type parameter, so there is a natural way to include the type parameters.
Technical note: when we consider bounds we have to think about context parameters again. For example, in List<X>, what is the upper bound on X? Well in Java it would be Object, but we need an owner, so we could follow OGJ and assume the owner is implicitly present, ie, the upper bound is x:Object where x is an implicitly declared, fresh formal context. Or we could use existential types, ie, the upper bound is \exists x.(x:Object), or in wildcard syntax, ?:Object.
Just looking at the existential types syntax there makes me wonder if it should be (\exists x.x):Object or \exists x.(x:Object), and if there is any difference, and even what the precise meaning of the former is (which are kind of left over questions from the Jo\exists paper that I should think about answering).
No comments:
Post a Comment