<!DOCTYPE html><html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body><div style="font-family: sans-serif;"><div class="markdown" style="white-space: normal;">
<p dir="auto">This is a major step forward. I have three sets of comments overall.</p>
<h1 style="font-size: 1.4em;">Looking back…</h1>
<p dir="auto">First a bit of history here, as I recall it: When we started working on<br>
VM support for Valhalla, I remember very early conversations (2015-ish),<br>
involving Brian, Mark R., Guy S., Doug L., Dan H., Karen K., Dan S., etc.,<br>
in Burlington MA and Ottawa (IBM). During these conversations we had<br>
all manner of crazy ideas (as we still do today, TBH), including ornate<br>
new syntaxes for descriptors. Brian made the point that we should pick<br>
just one L-like descriptor to describe the new flavor of data, and so<br>
Q was born. Brian further said something to this effect, IIRC:<br>
“We won’t necessarily keep the Q forever, but it will help us, during<br>
prototyping, to clearly map all of the places where value-ness needs<br>
to be tracked.” I remember thinking, “OK, but we’ll never get rid<br>
of it; it’s too obviously correct.” One result of this was we were<br>
able to define everything about values in the VM more crisply and clearly.</p>
<p dir="auto">Another result was yearly struggle sessions about how we were ever going<br>
to handle migration of Optional, LocalDate, etc. I’m surprised and glad<br>
that we have come to a place of maximum erasure, where (a) all the places<br>
where Q-ness needs mapping have been mapped, and yet (b) there is now no<br>
remaining migration problem (despite no investment in high-tech API<br>
bridges).</p>
<p dir="auto">Along the way Dan S. started quietly talking about Type Restrictions,<br>
which seemed (at first) to be some high-tech ceremony for stuff that could<br>
just as easily be spelled with Q’s. I’m glad he persisted, because now<br>
they seem to be the right-sized bucket in which to place the Q-signals,<br>
after Q’s go away.</p>
<p dir="auto">So, although I am wistful to see that clarity of Q’s go, it is more with<br>
nostalgia than regret. We have the clarity they bought us. And (bonus)<br>
they seem to dovetail with the next giant task of Valhalla, which is<br>
coping with generic data structure specialization (|List<int>|).</p>
<h2 style="font-size: 1.2em;">Avoiding the slippery slope</h2>
<p dir="auto">Next, I want to point out that part of the trick of doing this well is<br>
not doing too much all at once. It’s not straightforward. Our newly<br>
won insights make it clear that we could do for |String!| what we<br>
propose for |Point!|, but if we take such incremental RFEs as they<br>
occur to us we will, in fact, be falling down a slippery slope towards<br>
a Big Bang of VM functionality that gets deferred further and further.<br>
(A Big Crunch would be a more likely outcome, frankly. Happily, we<br>
have learned to deliver incrementally, yes?) I would like to restate<br>
from Brian’s proposal a guiding principle to keep us off the slippery<br>
slope, until such time as we agree to take the next steps downward.</p>
<p dir="auto">I think one key principle here is to embrace erasure, and hide the<br>
presence of new refinement types from legacy code. (A nit: We should<br>
pick a phrase and stick with it. “Type refinements” or “refined types”<br>
are fine phrases, but it’s not clear they are exact synonyms with<br>
“refinement types”. Rather arbitrarily, I prefer “refinement type”,<br>
perhaps because it point to two realities: It’s a type, and there<br>
was a refinement decision made.</p>
<p dir="auto">Here is a complementary principle: In the VM, we should choose to support<br>
exactly and only those refinement types that support Valhalla’s prime goals,<br>
which are data structure improvement (flattening). Since |String!| doesn’t<br>
(yet) have a flattening story, |String!| should not be a (VM) representable<br>
type. Since |Integer!| is already covered by |int|, neither should |Integer!|<br>
be a (VM) representable type. (A programmer may get fewer mirrors than<br>
expected, but note that we are not adding any mirrors at all!) Although<br>
|Point![]| is a useful specialized data structure, |Point![][]| is not<br>
so useful; its usefulness stems from the structure of its components,<br>
not its own top-level structure. Therefore, making a distinction between<br>
|Point![][]| and |Point![]![]| (and |Point![][]!| and so on) is bookkeeping<br>
which we would have to pay for but which wouldn’t pay us back.</p>
<p dir="auto">This takes me to the following specific points about the Big Three use cases:</p>
<ul>
<li>
<p dir="auto">Field declaration - The refinement type can only be of the form |B3!|</p>
</li>
<li>
<p dir="auto">Array creation - The component type can only be of the form |B3!|</p>
</li>
<li>
<p dir="auto">Casting - The cast type can be either |B3!| or |B3![]|</p>
</li>
</ul>
<p dir="auto">I think Brian covered all that, except for the following lines, which I<br>
think are a mis-step (down that slope I mentioned):</p>
</div><div class="plaintext" style="white-space: normal;"><blockquote style="margin: 0 0 5px; padding-left: 5px; border-left: 2px solid #777777; color: #777777;"><p dir="auto">It is a free choice as to whether we want to translate a field of type
<br>
|Point![]| using an array refinement or fully erase it to |Point[]|.</p>
</blockquote></div>
<div class="markdown" style="white-space: normal;">
<p dir="auto">If we support |multianewarray| then it must take a CP reference to |B3![]|.<br>
But I don’t think that pulls its weight, so let’s not.</p>
<p dir="auto">Why does |checkcast| get extra powers not enjoyed by the other two use<br>
cases? I think the answer is pretty simple: |checkcast| is the last<br>
resort for a Java compiler’s T.S. (translation strategy); if some type<br>
cannot be represented on a VM container (and enforced by the verifier)<br>
then either it cannot be safely cast (leading to “unchecked” warnings)<br>
or else it must be dynamically checked (requiring a |checkcast|).</p>
<p dir="auto">In order for a Java cast like |(Point!)x| to be efficient, it seems<br>
that |checkcast| should pick up the the job in one go, rather than<br>
require the T.S. to emit first |Objects::requireNN| and then a |checkcast|.<br>
(Note also our self-imposed rules for avoiding library dependencies…)<br>
And having |(Point!)x| be unchecked would be far too surprising, yes?</p>
<p dir="auto">The case for an effective cast of the form |(Point![])a| is perhaps<br>
less obvious, but it it very useful (from my VM perspective) to<br>
let the programmer use it to communicate flattening intentions<br>
outside of a loop, before the individual |Point| values are read or<br>
written. So the T.S. puts a dynamic check on an initialized |Point![]|<br>
variable and then all the downstream code can “know” that flat access<br>
is being performed. Note that this design pattern works great for<br>
multi-dimensional arrays (at source level), except that the type<br>
|Point![][]| is uncheckable. I’m not sure how to explain this gap<br>
to users, but the VM-level reality is that the optimizations for<br>
flat access care only about arrays of dimension one, so I’m happy<br>
the gap is there. I hope we won’t be forced to fill it, because that<br>
will cause a large set of new compliance tests and a bug tail.</p>
<pre style="margin-left: 15px; margin-right: 15px; padding: 5px; background-color: #F7F7F7; border-radius: 5px 5px 5px 5px; overflow-x: auto; max-width: 90vw;"><code style="margin: 0; border-radius: 3px; background-color: #F7F7F7; padding: 0px;">Point![][] a2d = …; // T.S. cannot put checkcast on a2d, I hope
for (var a1d : a2d) { // T.S. puts checkcast on each a1d, I hope
for (var x : a1d) {
… process x …
}
}
</code></pre>
<p dir="auto">Another likely use of a |checkcast| of a both kinds of type is when<br>
the T.S. emits code to load from a field with of type |B3!| or<br>
|B3![]|.</p>
<pre style="margin-left: 15px; margin-right: 15px; padding: 5px; background-color: #F7F7F7; border-radius: 5px 5px 5px 5px; overflow-x: auto; max-width: 90vw;"><code style="margin: 0; border-radius: 3px; background-color: #F7F7F7; padding: 0px;">class C { B3! x; B3![] a; }
…
C c = …;
var x = c.x; // T.S. could put a checkcast here, if it helps
var a = c.a; // ditto
c.x = x.nextX(); // T.S. is very likely to put a checkcast here
c.a = Arrays.copyOf(a); // ditto
</code></pre>
<p dir="auto">Exactly where to put each |checkcast| (and where not to bother)<br>
is an interesting question; perhaps it’s too much work to place<br>
them on every read of a field. (I think it’s a good idea, because<br>
redundant checks are free in the VM and earlier checks are better<br>
than later ones.) But it seems very likely that at least field<br>
writes will benefit from checkcasts, for all types that are<br>
representable. And, note that type of <code style="margin: 0; padding: 0 0.4em; border-radius: 3px; background-color: #F7F7F7;">new B3![]</code> is representable.<br>
Its class will be <code style="margin: 0; padding: 0 0.4em; border-radius: 3px; background-color: #F7F7F7;">B3[].class</code>, but its representable type<br>
will be something like <code style="margin: 0; padding: 0 0.4em; border-radius: 3px; background-color: #F7F7F7;">NullRestrictedArray.of(B3.class)</code>.</p>
<h2 style="font-size: 1.2em;">Healing the rift?</h2>
<p dir="auto">One goal that is being held loosely at this moment is the old<br>
promise of Valhalla to “heal the rift” between |int| and |Integer|.<br>
(More generally, between primitives and references.) We’ve come<br>
this far, are we going to give up on that goal now?</p>
<p dir="auto">By choosing not to allow |RefinementType| mix with |Class|, we<br>
are committing to leaving |int.class| and other primitive classes<br>
(and |void.class|) by themselves as outliers among the “proper” classes<br>
and interfaces (|C.class|, |I.class|) and “array classes” (|T[].class|).<br>
That’s not a rift-healing move, but it doesn’t have to interfere with<br>
other rift-healing moves that we <em>could</em> do.</p>
<p dir="auto">I don’t think there is a rift-healing move we could do with field<br>
declarations, since flat |int| fields are already fully supported.</p>
<p dir="auto">Although it is technically an incompatibility, we might consider<br>
allowing legacy |int[]| arrays to interoperate with |Object[]|,<br>
so that more generic code can be written. That would be close to<br>
the spirit of allowing |B3![]| arrays be viewed transparently as<br>
possibly-null-tolerant |B3[]| arrays.</p>
<p dir="auto">But there is definitely a slippery slope here. Should |int[]|<br>
be a subtype of |Object[]|? I think that also would be required.<br>
I would like to do this, if possible.</p>
<p dir="auto">(There is no cause to ask that |int|, which isn’t even a reference<br>
type, should somehow be made to look like a subtype of |Integer|.)</p>
<p dir="auto">One rift-widening move I’d like to avoid is introducing a third<br>
representable type, between |int| and |Integer|, for the purpose<br>
of making flat arrays of |Integer| that are not |int| arrays.<br>
Any “value-ification” of |Integer| should avoid that trap.<br>
Rather |Integer![]|, if it is representable at all, should be |int[]|.</p>
<p dir="auto">I guess Dan S. is tracking these issues; I don’t recall them being<br>
discussed recently, but maybe they will ripen after we get closure<br>
on the bigger questions about Q.</p>
<p dir="auto">There is another place where a “heal the rift” move might make sense,<br>
and that is in the API for |Class|. Brian suggests that perhaps the<br>
|Class::cast| method could be lifted to |RepresentableType|. That<br>
will make it easier to reflectively emulate |checkcast| instructions,<br>
but it will give wider exposure to an existing sharp edge in the<br>
|Class| API, which is the non-functionality of primitive mirrors.</p>
<p dir="auto">(I suppose Brian’s mention of lifting |cast| is why I’m getting into<br>
the question of “healing rift” at all. Pulling on that string brings<br>
us to the that rift, IMO.)</p>
<p dir="auto">I mean that the call |int.class.cast(x)| does not work, and lifting<br>
that non-behavior up to |RepresentableType| will make a new and<br>
unwelcome distinction between |B3!| and |int|: The mirror for |B3!|<br>
would (presumably) do a null check and cast to |B3|, while the mirror<br>
for |int| would fail. Here are options to handle this sharpened edge:</p>
<ul>
<li>Leave it as is. Sorry if you accidentally used |int.class|.</li>
<li>Enhance |int.class::cast| (and |isInstance|) to check for |Integer|.</li>
<li>Deem |cast| not liftable; make a new |RepresentableType::checkType|<br>
(and |isType|), and have it be total over B1/B2/B3 and primitives (B0??).</li>
</ul>
<p dir="auto">Enhancing |int.class::cast| is arguably in the same spirit as allowing<br>
|int[]| to be a subtype of |Object[]|.</p>
<p dir="auto">But I think I prefer the last. In any case, I don’t look forward to a<br>
widening rift between primitives (B0!) and the other types.</p>
</div></div></body>
</html>