On 28/04/2021 17:48, Brian Goetz wrote:
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.
I think I get this - but I guess this implies that, in my previous example:
Foo x = ...
if (x instanceof Bar)
The instanceof will not be considered total, and therefore be accepted
by the compiler (sorry to repeat the same question - I want to make sure
I understand how totality works with sealed hierarchies).
If that's the case, I find that a bit odd - because enums kind of have
the same issue (but we have opted to trust that a switch on an enum is
total if all the constants known at compile time are covered) - and, to
my eyes, if you squint, a sealed hierarchy is like an enum for types
(e.g. sum type).
That said, I think this discussion kind of demonstrates that reasoning
about totality is not that straightforward; I believe you can see why I
jumped to the conclusion that Box<Soup> must have been total on
Box<Lunch> (if Soup was the only permitted concrete subtype of Lunch) -
but it turned out I was barking up the wrong tree. This is surely
caused, in part, by the fact that I'm less immersed in pattern-land
(e.g. more an interested follower at a distance); but I think it also
reflects some genuine complexity when it comes to reasoning about totality.
Anyway, backing up - this below:
```
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();
}
```
is good code, which says what it means. I think the challenge will be to
present error messages (e.g. if the user forgot to add case Box(null))
in a way that makes it clear to the user as to what's missing; and maybe
that will be enough.
Maurizio
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
