Null restricted type and JSpecify

[John Rose]

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.

— John