I'll chime in that I am coming around to disjoint Q/L, and here are a couple of thoughts on how to reconcile that with VM generics.
On Jan 27, 2022, at 2:00 PM, John Rose <john.r.r...@oracle.com<mailto:john.r.r...@oracle.com>> wrote: Furthermore, i believe that subtyping is a key to avoid multiple bytecode verification of the generics code. I recommend a far simpler technique: Just don’t. Don’t multiple-verify, and and don’t do anything that would need such extra verification (with different types) to give the same answer (as the first verification). Also, don’t think of a JVM-loaded set of bytecodes as every having more than one operational meaning. (I don’t understand this obsession, not just with you, of imagining generic bytecodes as statically “recopied” or “recapitulated” or “stamped out” for each generic instance. I think it's an important aspect of parametric polymorphism that properties that are true in the generic code continue to be true for specific instantiations. (It's complicated, I'm not making a formal rule here, but there's an intuition there that I think is right.) So the key for me is: if the generic code says you're going to aload a Ljava/lang/Object and then store it with putfield, it should be true that, *modulo optimizations*, all instantiations will load an Object and store it in an Object field. That doesn't mean we're literally verifying it for each instantiation, but it's how I expect code authors to understand what they are saying. By example, with the TypeRestriction attribute [1], the restriction has to be subtype of the declared type/descriptor. No, just no. (Not your fault; I suppose the TR docs are in a confusing state.) There’s no reason to make that restriction (linking TRs to the verifier type system), other than the futile obsession I called out above. And if you do you make yourself sorry when you remember about the verifier’s I/J/F/D types. And for many other reasons, such as instance types which are inaccessible to the generic code. And the simple fact that bytecodes are not really generic-capable, directly, without serious (and futile) redesign. Making bytecodes directly generic (in the sense of contextually re-type-able) is never going to be as simple as using a TR mechanism which occurs apart from the verifier. A “type system” for TRs is pretty meaningless, from the JVM POV. In the JVM, a TR (despite its name) is most fundamentally an operational specification of how to project (G->I) or embed (I->G) instance types into generic types. It’s a function pair. It can connect I=int to G=Object, which the JVM knows are disjoint types. I do think it's important that type restrictions are polymorphic: if there's a type restriction on my above Object, it should *both* be true that the value is an Object, and the value has whatever property the type restriction claims. A type restriction can't make the value no longer an Object. But I think we can hold on to this property and still support disjoint Q/L. How? By not allowing type restrictions to literally claim that values have Q types. Instead, they claim that a value with some L type is *freely convertible to* a particular Q type. (This may be the same thing as John saying the type restriction involves projections and embeddings, although I'm not sure I would make it the type restriction's responsibility to encapsulate those conversions.) So, for example: a type restriction that we might spell as 'QPoint' (and maybe that notation is a mistake) is an assertion that a particular L-typed variable always stores non-null objects for which 'instanceof Point' is true. *But they're still objects*, as far as the abstract JVM is concerned. Then the JVM implementation is free to recognize that it can use the same encoding it uses for the actual type 'QPoint' to store things in the variable. There are a couple places where reality intrudes on this simple model: - The initial value of a field/array with a type restriction is determined by that type restriction (because, e.g., 'null' can't satisfy the 'QPoint' restriction) - Type restrictions may introduce tearing risks, which would have to be explained by specifying the possibility that a JVM implementation may use type restrictions to optimize storage of value object instances of primitive classes, encoding them as primitive values I'm left feeling somewhat uneasy that we end up with a world in which directly-typed code has Q types, while specialized generic code has <non-null instances of primitive classes> as its "types"—two different ways to explain the exact same thing, in some sense duplicating efforts—but I think we can live with that. On the other hand, it's a nice win that the language runtime model is more closely aligned with the JVM's runtime model (where value objects and primitive values are two distinct things).
