"Model 2" prototype status

[Gavin Bierman]

Hi Timo,

> On 2 Aug 2015, at 21:55, Timo Kinnunen <timo.kinnunen at gmail.com> wrote:
> 
> Hi, 
> 
> Re: “I don't care about the syntax but the one you propose doesn't help IMO.”
> 
> I have to agree. You really get a sense that there is no overall design behind this syntax backing it up. 
> 
> For example, my current source of confusion is whether A<any T> is to be interpreted as A<ref T | any T | null> or as A<ref T | any T | !(null)>. (A note on the syntax being used: the presence  or absence of the nulltype amongst the bounds is to be interpreted literally.)
> 
> Seeing “Alternately, you can interpret "any T" as a union bound ("T extends Object | value")” suggests it’s the first interpretation that’s correct but then seeing “ Some operations that are allowed on ordinary tvars are not allowed on avars, such as assigning a T to an Object, assigning null to a T, etc.” suggests the correct interpretation should be the latter.
> 
> 
> A properly designed syntax where such semantics can be expressed in a natural way will be helpful to have, one year from now. Would be much more helpful to have it right now though, IMHO…

As I’m the semantics guy on the design team your request for semantics got my attention :-) (Plus I’d like to reassure you that there are hundreds of hours of thinking about the design so far; and many more to come!)

Here’s a semantic take on what’s going on: A type is a set of values. In Java when declaring variables we are used to declaring their type, e.g. `Bar x`. A _sort_ is a set of types. Currently in Java when declaring type variables we do not declare their type/sort; it’s implicit, and is the set of all reference types. (Some languages do let you define the sorts of type variables, e.g. Haskell.) Of course we can constraint the set further with bounds, but morally type variables have a type/sort.

In Valhalla we will be in the world where some type variables will range over all reference types, and some over other sorts. It’s this 'other sorts' stuff that is new. In our experiments, we have identified three useful sorts: (i) `any` the sort containing all types, (ii) `ref` the sort containing all reference types (currently, the only sort denotable in Java), and (iii) `val` the sort containing all value types (currently the eight primitive types, but we are also experimenting with supporting user-defined value classes). We currently adopt a similar syntax for sort declarations as for type declarations, e.g. `ref X`, although other syntax choices could be taken from other languages, e.g. `X::ref`. We’re trying not to get too bogged down with syntax right now, but the idea should be clear.

Placing a sort on a type variable in, for example, a class declaration can have consequences in the declaration body. If you declare a class `Pop<any T>` you are declaring it *for all* instantiations of T, including primitives. Hence in the body of declaration, you shouldn’t be able to assign null to an instance of the type variable, for example. It breaks the contract in the declaration. This is no different to Java 8, where we check in the body that we respect the bounds contract on type variables. 

Given that wildcards are a form of existential type, corresponding to the three sorts are three forms of wildcards: (i) `Foo<any>` which denotes any type instantiation of `Foo`; (ii) `Foo<ref>` which denotes a reference type instantiation of `Foo` (this is currently written `Foo<?>` in Java); and (iii) `Foo<val>` which denotes a value type instantiation of `Foo`. Again, our syntax is preliminary; we could write these as `Foo<any ?>`, `Foo<ref ?>` and `Foo<val ?>`, for example.

[BTW: Currently the prototype doesn’t support the `val` sort, but I wanted to add it to help you see what we’re up to.]

I’m working on a more formal definition of the design and the translation strategy, which I can share with you when it’s ready, if you like. (It’ll look something like this: http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf <http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf>)

Hope this helps,
Gavin