Null restricted type and JSpecify

[forax at univ-mlv.fr]

----- Original Message -----
> From: "John Rose" <john.r.rose at oracle.com>
> To: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "valhalla-spec-experts" <valhalla-spec-experts at openjdk.java.net>
> Sent: Wednesday, November 30, 2022 7:21:24 PM
> Subject: Re: Null restricted type and JSpecify

> On 30 Nov 2022, at 9:06, forax at univ-mlv.fr wrote:
> 
>> ----- Original Message -----
>>> From: "John Rose" <john.r.rose at oracle.com>
>>> To: "Remi Forax" <forax at univ-mlv.fr>
>>> Cc: "valhalla-spec-experts" <valhalla-spec-experts at openjdk.java.net>
>>> Sent: Wednesday, November 30, 2022 6:01:42 PM
>>> Subject: Re: Null restricted type and JSpecify
>>
>>> Kevin & co won’t like this maybe, but I think this design and our Valhalla
>>> design do not conflict, precisely because they make completely distinct sets of
>>> assertions, and yet the assertions (taken together) are consistent.
>>>
>>> What we are talking about here is X! on non-type-vars.  That means we are adding
>>> a state EXPLICIT_MINUS_NULL, which (a) has an obvious relation to the other
>>> states in JSpec., and (b) can have a semantic weight different from anything in
>>> JSpec.; it can and should translate to a different Q-descriptor.
> 
> Disclaimer!  By the way, my use of X! doesn’t imply a particular bikeshed for
> the syntax. JSpec. spells it @NonNull, one draft of Valhalla spells it .val
> (as in Point.val), and “everybody knows” what X! means, kind of.  Except they
> don’t:  Different languages give very different meanings (sometimes in very
> subtle details) to their emo-type syntaxes.  There!
> 
>>
>> if it's L-descriptor in descriptors but Q-descriptor in TypeRestriction +
>> bytecodes, yes !
>>
>> I think being able to add a '!' if you have overlook one should be an option.
> 
> As we discussed in the EG just now, this is a distinct proposal which should
> be taken up independently of anything we do regarding JSpecify.
> 
> At the VM level, we are planning to do (for generics) some sort of type
> restrictions which are semantically enforces but DO NOT appear in the
> descriptor; it is a side channel to the descriptor.  So L-Point could
> be a translation of Point.val (aka Point! but see above) instead of
> Q-Point, as long as there is a type restriction lurking somewhere near
> that specific occurrence of L-Point.
> 
> Technically we could do this at some level.  But I’d like to challenge
> this proposal, by a counter-proposal that (I think) would first have
> to hold water, in order to translate Point.val as L-Point+TR.  That
> counter proposal is, experimentally amend today’s Java translation
> strategy so that every use the descriptor I (for int) in APIs is
> changed to L-Integer plus a TR, so that (basically) int erases to
> Integer, with a TR.  Suppose some reasonable JVM support for TRs
> of this form (just for primitive types, for now).  Now, can you
> implement the JLS?  Should you do it this way?
> 
> For bonus points (as you suggested in the meeting) see if you can
> erase ALL TYPES to L-Object, with associated TRs.  Does it work?
> Would it be smart?
> 
> If these experiments would go wrong somehow, I suggest, strongly,
> that a similar voyage into erasure for Q-Point into L-Point+TR
> would also go wrong, in similar ways.
> 
> For starters, some overloaded functions would be broken in either
> of those thought experiments.  That should make us a little bit
> scared to do that same thing for the new Q-types.  I suspect there
> are a number of “gotchas” like this.  We spent the first couple
> of years on the Valhalla project enumerating such gotchas, for
> various proposals.  Generally speaking it has turned out that
> erasing Q to L seems OK about 80% of the way through the details,
> and then something jumps out and bites, related to details of the
> JLS, or JVM optimizations, or binary compatibility, or all three
> at the same time.
> 

I wonder if you are making the problem harder than it is.

Valhalla can be decomposed into 3 goals,
1) Provides value/primitive classes
2) Heal the rift between primitive classes and primitive types
3) Provides generics over value/primitive classes

I believe that wanting all primitive classes (or worst all value classes) to behave/be potential primitive types is a kind of over-generalization.

Let's summarize the difference between a primitive type and a primitive class
- a primitive type has a special kind of descriptor, a special kind of opcodes (iload vs aload), special kind of arrays (anewarray vs newarray), etc
- a primitive type has a special kind of runtime mirror (int.class, double.class, etc)
- a primitive type has a special kind of ==, <, >, etc (float/double semantics (IEEE 754) is not compatible with Float/Double semantics)
- a primitive type is always flattened

Some of the differences are historical accidents but for me, the major difference between a primitive class and a primitive type is that flattening is *guaranteed* for a primitive type and the fact that it has its own descriptor and bytecodes is a direct consequence of that decision.

So in term of translation strategy, wanting value/primitive classes to be translated in bytecode with the same properties for overloading, etc than primitive types should not be a goal.

> — John

Rémi