“We won’t necessarily keep the Q forever, but it will help us, during
prototyping, to clearly map all of the places where value-ness needs
to be tracked.” I remember thinking, “OK, but we’ll never get rid
of it; it’s too obviously correct.”


Or, if not too obviously correct, too nuisancefully attractive.  We all got comfortable with the Qs, and when it was time to give them up, we all resisted (for different reasons.)  For me, what sold me here is the degree to which we are aligning with the language model, and how it seems a shorter hop from here to enforced `String!` putfields and to species.

Another result was yearly struggle sessions about how we were ever going
to handle migration of Optional, LocalDate, etc. I’m surprised and glad
that we have come to a place of maximum erasure, where (a) all the places
where Q-ness needs mapping have been mapped, and yet (b) there is now no
remaining migration problem (despite no investment in high-tech API
bridges).


Indeed, I remember a time when we thought "we might be able to migrate Optional to B2, but never to B3", and Kevin thought I was crazy to even imagine that.  The various moves have been like the rebalancing of an AVL tree; as you rotate left, then the left side is unbalanced, and you rotate the left subtree right, and then ...

Along the way Dan S. started quietly talking about Type Restrictions,
which seemed (at first) to be some high-tech ceremony for stuff that could
just as easily be spelled with Q’s. I’m glad he persisted, because now
they seem to be the right-sized bucket in which to place the Q-signals,
after Q’s go away.


Yeah, sounded like magic pixie dust at first to me too.

To me, the huge (implementation-driven) breakthrough was discovering that we could effectively scalarize L-value arguments and returns in the calling convention, at almost no extra cost over Q.  This surprised me, and is what cracked the nut open that we could erase more aggressively.  (Thanks Tobias!)

I think one key principle here is to embrace erasure, and hide the
presence of new refinement types from legacy code.


Indeed, the biggest temptation is the "but we can, and it might be useful."  Leaving the level of Class (and descriptors) alone and working entirely at the next level down feels unnatural.

Here is a complementary principle: In the VM, we should choose to support
exactly and only those refinement types that support Valhalla’s prime goals,
which are data structure improvement (flattening). Since |String!| doesn’t
(yet) have a flattening story, |String!| should not be a (VM) representable
type.


I'd agree, but only if I can add "yet".  We should pathfind through the VM using the things we know we need now, but if we can harness value set restrictions later, this is a huge step towards aligning to the user model, where users will be beating down our door for `String!` and either living without it, or with a complex set of compiler-inserted, only-mostly-reliable checks.

Why does |checkcast| get extra powers not enjoyed by the other two use
cases? I think the answer is pretty simple: |checkcast| is the last
resort for a Java compiler’s T.S. (translation strategy); if some type
cannot be represented on a VM container (and enforced by the verifier)
then either it cannot be safely cast (leading to “unchecked” warnings)
or else it must be dynamically checked (requiring a |checkcast|).


Compilers need checkcast when they use erasure; we're using a lot of erasure here, so we need the biggest checkcast we can get.

Exactly where to put each |checkcast| (and where not to bother)
is an interesting question; perhaps it’s too much work to place
them on every read of a field. (I think it’s a good idea, because
redundant checks are free in the VM and earlier checks are better
than later ones.) But it seems very likely that at least field
writes will benefit from checkcasts, for all types that are
representable. And, note that type of |new B3![]| is representable.
Its class will be |B3[].class|, but its representable type
will be something like |NullRestrictedArray.of(B3.class)|.


Spoiler: I much prefer to check on write, and ultimately, push that check into the VM using the same value set restriction machinery as we do for B3!.

I don’t think there is a rift-healing move we could do with field
declarations, since flat |int| fields are already fully supported.


We could be generous in linkage, treating "I" and "LInteger;" with a type restriction as the same type, but it doesn't seem worth it.

Although it is technically an incompatibility, we might consider
allowing legacy |int[]| arrays to interoperate with |Object[]|,
so that more generic code can be written. That would be close to
the spirit of allowing |B3![]| arrays be viewed transparently as
possibly-null-tolerant |B3[]| arrays.


I think we concluded that this was probably a forced move at some point, but we should revisit that analysis.

(There is no cause to ask that |int|, which isn’t even a reference
type, should somehow be made to look like a subtype of |Integer|.)


Yes, but its arrays may be a different story.

I mean that the call |int.class.cast(x)| does not work, and lifting
that non-behavior up to |RepresentableType| will make a new and
unwelcome distinction between |B3!| and |int|: The mirror for |B3!|


(not actually a mirror)

Reply via email to