Patterns and nulls

[John Rose]

Good write-up; this is tricky reasoning and needs to be presented in a block,
or we'll spend the next several months answering one-line emails that start
"Why didn't you just…".  See also:
  https://blogs.oracle.com/jrose/feynmans-inbox <https://blogs.oracle.com/jrose/feynmans-inbox>

Here are a few extra footnotes, to amplify the argument.

On Mar 14, 2018, at 9:58 AM, Brian Goetz <brian.goetz at oracle.com> wrote:
> 
> ...The "la la la" approach has gotten us pretty far…

This "la la la" works great for the null-free coding style, which many
of us try to stay within.  It stinks for the null-using coding style,
which sometimes we choose and sometimes is forced on us
by APIs for which null is a significant value.  We're not going
to suddenly pick a winning style, so our design must include
support for both styles.  "But it is tolerated so well for legacy
switch" is not a valid objection, since we are making a pattern
facility that goes far beyond legacy types and includes other
operations which already *do* tolerate nulls (cast, instanceof).

> ...But if you pull on this string a bit more, we'd also like to do the same at the top level, because we'd like to be able to refactor…

And also because the null-using style is legitimate in Java.
Null-haters may groan, but we must have patterns which "know
about" null so null-users can gracefully thread their null values
through the new constructs (where it makes sense of course).

(BTW, anybody who uses Map::get is a null-user, at least briefly.)

> ...So, we want at least some type patterns to match null, at least in nested contexts.  Got it.

(Also, null-users will object strongly if we excise null from the value
space of "var" and similar constructs which don't appear to incorporate
null checks in other places.  They will say, "stop checking my nulls
for me by default; either I want them, or I have some other coding
practice for diagnosing accidental nulls".  The null-haters won't be
benefited much by the extra checks either; presumably they have
a more aggressive set of checks embedded in their code style.)

> 
> … So we can _define_ `T t` to mean:
> 
>     match(T t, e : U) === U <: T ? true : e instanceof U
> 
> In other words, a total type pattern matches null, but a partial type pattern does not.

Type test patterns smuggle instanceof into the world of patterns.
Instanceof, for very good reasons, does not recognize null.
If you go ahead and cast the null, the language will let you,
but the common combo of instanceof/checkcast, which is what
narrowing type patterns embody, does not accept nulls.
If you are consciously narrowing a wide reference to a narrow
type, you know the narrowing might fail, and you also know
you won't get nulls there.  These are rules that both null-users
and null-haters can live with easily.  If on the other hand you
are just binding a reference to the same type (or a super),
then you know it's not a narrowing, and it can't fail, and so
any nulls (love 'em or hate 'em) will get through.

This, this design depends on the fact that programmers are
usually aware (and also their IDEs are aware) of which type
occurrences are partial and which are total.  With patterns
the distinction is a little more subtle, but we think it will be
obvious in practice.

(Yes, you can make puzzlers here.  Even |,& expressions
can pose NP-hard problems and long identifier spellings can
encode messages in binary.  But abusus non tollit usum;
the abuse doesn't invalidate the use.)

> ...
> There's more work to do here to get to this statically-provable null-safe switch future, but I think this is a very positive direction.  (Of course, we can't prevent NPEs from people matching against `Object o` and then dereferencing o.)

(Those null-users!  They get what's coming to them.)

> Instanceof becomes instanceof
> -----------------------------
> 
> The other catch is that we can't use `instanceof` to be the spelling of our `matches` operator, because it conflicts with existing `instanceof` treatment of nulls.  I think that's OK; `instanceof` is a low-level primitive; matching is a high-level construct defined partially in terms of instanceof.

Above I claimed that people already know the difference
between types which are partial and those which are total.
In the case of instanceof, ask yourself what you would think
if you saw this code:

    if (x instanceof Object)  System.out.println("got an object");

Most programmers would feel something was wrong, since the
instanceof is never followed by Object.  They might look upward
in the file to find out what is the strange type of x.  After puzzling
for a while they might figure out how the code works; some wouldn't.
I claim that their initial unease comes from their familiarity with
Object as a total type, and finding this total type in a partial
position (after "instanceof").

And of course programmers know what happens when you
use a partial type as if it were total:

   String x = myObject;

First the IDE turns red and then you get a javac error.
The fix puts String into a partial construct, a cast.

Someone will point out at this point that the partial/total
distinction is determined by context; if "myObject" is a
string, then the above assignment is OK and "instanceof
String" is paradoxical in the same way as "instanceof
Object".  To which we can only reply, yes, you noticed.
Constructs in Java rely on context for their meaning,
and you don't always put extra markings on the uses
to signal the meanings.  It's a matter for experiment
to find out whether people's sense of partial vs. total
will extend to patterns.  We think there will be enough
contextual cues in real-world code (like, "this pattern
came last and the compiler didn't complain!") to keep
things straight.  And IDEs will help also.

So, Brian's rule for type pattern matching breaks type
patterns apart in a way programmers are already
experienced with, and assigns the expected behavior
to each half.  This behavior is neutral with respect to
both null-hating and null-using code.  For this reason,
switches built on top of it are also neutral.  What's more,
their type test patterns commute correctly.

That looks a lot like winning to me.  Let's try it.

— John
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20180314/a7633218/attachment.html>