On Jun 8, 2021, at 2:21 PM, Dan Smith <daniel.sm...@oracle.com> wrote:
>
> Please see this JEP draft:
>
> http://openjdk.java.net/jeps/8261529
>
> This is the third anticipated piece in our initial suite of Valhalla preview
> features (along with JEPs 401 and 402). It's also the first step in the
> revised generics story, to be followed up in the future with JVM enhancements
> for better performance (including species & type restrictions).
>
> This is entirely a language enhancement, and will be experienced by
> developers as a number of new warnings for generic classes and methods.
> Addressing the warnings makes generic APIs interoperate smoothly with
> primitive value types and prepares them for the future JVM enhancements.
I like this JEP. I think it proposes reasonable
tactics for repositioning type variables for
success with Valhalla.
From the way it reads (notably, where it
says syntax is subject to change), it seems
a provisional design, to be validated by
actual experience using the language
features to create new library APIs and
adapt existing ones to help deal with
null pollution gracefully. To put it
negatively, I don’t fully trust the
design here, until we have a chance
to use it for some time with real APIs.
But I think it’s very reasonable first
cut.
One item that is a wrong note for me
is the place where you say, “The proof
is similar to the control-flow analysis
that determines whether a variable has
been initialized before use.” I know
something about those proofs, having
contributed the “definite unassignment”
rules in Java 1.1. The basic rules do not
produce different answers along diverging
control paths (such as the “then” and
“else” sides of an if). The rules for
flow-based assignment in pattern
matching do something like this,
with the “assigned when true” type
clauses, but they are tied to new
testing sytnax (instanceof patterns).
But null testing can be done in many
ways, and so there is no “bright line”
for determining if a variable is null
or not on a taken path. It’s a slippery
slope. If you look at null-checking
frameworks, or JITs, you’ll see dozens
of rules regarding null deduction.
Also, none of the existing DA/DU
rules *change* the type of a variable;
they just make it available or not
available, but you are promising a
rule which makes the *same* variable
nullable along some paths and not
nullable along others. That’s not
a small or incremental change on
the existing language machinery.
All this is to say, I don’t think you
can display a clean proof, based on
a clean language design, that will
get what you are claiming.
I have a better proposal instead:
Just make sure it is possible to build
user-defined API points which have
the appropriate null-isolation effects.
For example, this should type-check,
and should be a usable idiom for
statically checked null control:
foo(T.ref xOrNull) {
T x = Objects.requireNonNull(xOrNull);
}
The internals of Objects.requireNonNull
probably contain an unchecked cast from
T.ref to T, where the language cannot “see”
the invariant, but the programmer can.
A @SuppressWarnings completes the story.
A similar point might work for the API of
Class.cast, if we can figure out how to
find the right Class witnesses:
foo(Class<T> witness, T.ref xOrNull) {
T x = witness.cast(xOrNull);
}
foo(Class<? extends T.ref> witness, T.ref xOrNull) {
T x = witness.valueType().cast(xOrNull);
}
(The fact that valueType returns NONE instead
of self is a problem here.)
The rules for instanceof can also be adjusted
to narrow from a target of T.ref to a variable
binding of T. This is (IMO) a better use of
language complexity than an open-ended
hunting season for nulls.
Anyway, I think the above ideas are less
of a blind alley than promising magic
flow checking of nulls.
— John
