The set of patterns { Box(Soup) } is considered total on Box<Lunch>
_with remainder { null, Box(null), Box(novel) } _.
The pattern Box(Soup) on its own is total on Box<Soup> (as opposed to
Box<Lunch>), with remainder { null }; we'll still NPE if the Box itself
is null.
The intuition here is that Lunch is still a more abstract type than
Soup, even if the implementation says "only soup here". We know that
this assumption could be violated before we get to runtime.
A normalizing force here is we want the same thing at top level and
nested level. If i have:
Lunch lunch = ...
switch(lunch) {
case Soup s:
}
I should expect the same null treatment as I do in the lifted case:
Box<Lunch> box = ...
switch (box) {
case Box(Soup s): ...
}
Which we get! In the first case, the _single pattern_ Soup is not
individually total on Lunch (Lunch is more abstract), but the _set of
patterns_ { Soup } is total on Lunch with remainder { null, novel
subtype of Lunch }, due to sealing, so we are able to conclude the
switch itself is exhaustive (with some remainder rejected.) When we
lift, we get totality with remainder of { Box(null), Box(novel) }, plus
also { null } because of the lifting.
On 4/28/2021 12:33 PM, Maurizio Cimadamore wrote:
On 28/04/2021 17:29, Brian Goetz wrote:
I assume that you are saying Box permits Soup only. But your
assumptions about "where do the nulls go" here are not right.
Box(Soup) does not match Box(null); the set of patterns { Box(Soup) }
is total on Box(Lunch) _with remainder Box(null)_. So the null paths
in this example are dead. (Also missing break statements.) So
rewriting, this switch is really equivalent to:
switch (lunch) {
case Box(Soup s):
System.err.println("Box of soup");
break;
case Bag(Soup s):
System.err.println("Bag of soup");
break;
/* implicit */
case Box(null), Bag(null): throw new NPE();
}
and the switch is total on Container(Lunch) under the Lunch=Soup,
Container=Box|Bag assumptions.
I have to admit that this is surprising.
So, if I have a sealed hierarchy that only permits one concrete type:
interface Foo permits Bar
doing:
Foo x = ...
if (x instanceof Bar)
is not considered a total instanceof?
Maurizio
