----- Original Message ----- > From: "John Rose" <[email protected]> > To: "Remi Forax" <[email protected]> > Cc: "valhalla-spec-experts" <[email protected]> > Sent: Wednesday, November 30, 2022 7:21:24 PM > Subject: Re: Null restricted type and JSpecify
> 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. > 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
