Re: "Model 2" prototype status

Timo Kinnunen timo.kinnunen at gmail.com
Mon Aug 3 23:38:55 UTC 2015


Hi, 


Thank you very much for writing up this detailed description! Indeed, it was the bit of syntax for <val T> that I was missing. With that in place, then using my syntax:


class A<any T>  {} 

== class A<T extends Object | null | val T> {} 

== class A<ref T | null | val T> {}

and 

class B<ref T | null> extends A<T> {} // is valid




class C<val T> extends A<T> {} // is valid

class D<any T> extends B<T> {} // not valid


And now things make a lot more sense.



The reason I’m keeping the special null type from §4.1 as a separate bound rather than having it folded inside <ref T> is that it lets the other possible combinations of bounds to have useful semantics attached to them. A <ref T> (the null type of §4.1 is specifically not included in the bounds!) would be the target type of primitive boxing conversion, and <val T | null> would be the target type of a value boxing conversion. Once these can be expressed, expressing the conversions itself becomes possible too.


Those tools available, it would now be possible to do better than treating the union type <ref T | null | val T> as the intersection type <ref T & null & val T> within the default implementation. Might as well, as this intersection type is usually empty anyway. To do better any needed conversion methods can be included as abstract stud methods to be compiled against.


Alas, I don’t get the impression that the design of the syntax has being able to express and explore semantics like these that can come up during the design of value types as one of its main goals. Instead the goals seem have more to do with the prototype being able to demonstrate which road it’s currently taking. The result of this is that it makes discussing the “roads that weren't taken” quite difficult and independently verifying them later almost impossible.





-- 
Have a nice day,
Timo.

Sent from Windows Mail





From: Gavin Bierman
Sent: ‎Monday‎, ‎August‎ ‎3‎, ‎2015 ‎15‎:‎43
To: Timo Kinnunen
Cc: Rémi Forax, Brian Goetz, valhalla-dev at openjdk.java.net




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)

Hope this helps,
Gavin


More information about the valhalla-dev mailing list