VM model and aconst_init

[forax at univ-mlv.fr]

> From: "Brian Goetz" <brian.goetz at oracle.com>
> To: "daniel smith" <daniel.smith at oracle.com>, "John Rose"
> <john.r.rose at oracle.com>
> Cc: "Remi Forax" <forax at univ-mlv.fr>, "valhalla-spec-experts"
> <valhalla-spec-experts at openjdk.java.net>
> Sent: Saturday, January 29, 2022 6:40:13 PM
> Subject: Re: VM model and aconst_init

> I think we're kind of stuck with a model like this, whether we admit it or not,
> because we have to allow for pervasive erasure and be able to fall back to
> looser linkage conventions. SO the type restriction was always optimistic; we
> might say "Object restricted to QPoint", but someone could show up and say
> "what's a restriction?" and then we have to respond "I said Object, sir".
yes, because of raw types/erasure or wildcard types ! 

Rémi 

> On 1/28/2022 1:00 PM, Dan Smith wrote:

>> 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).