On 30 Nov 2022, at 9:06, [email protected] wrote: > ----- Original Message ----- >> From: "John Rose" <[email protected]> >> To: "Remi Forax" <[email protected]> >> Cc: "valhalla-spec-experts" <[email protected]> >> 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
