[pattern-switch] Exhaustiveness

[Brian Goetz]

>
>  - Exhaustiveness and null. (Tagir)  For sealed domains (enums and 
> sealed types), we kind of cheated with expression switches because we 
> could count on the switch filtering out the null.  But Tagir raises an 
> excellent point, which is that we do not yet have a sound definition 
> of exhaustiveness that scales to nested patterns (do Box(Rect) and 
> Box(Circle) cover Box(Shape)?)  This is an interaction between sealed 
> types and patterns that needs to be ironed out.  (Thanks Tagir!)

[ Breaking this out from Tagir's more comprehensive reply ]

> It's unclear for me how exhaustiveness on nested patterns plays with
> null. case Box(Circle c) and case Box(Rect r) don't cover case
> Box(null) which is a valid possibility for Box<Shape> type.

It’s not even clear how exhaustiveness plays with null even without 
nesting, so let's start there.

Consider this switch:

switch (trafficLight) {
case GREEN, YELLOW: driveReallyFast();
case RED: sigh();
     }

Is it exhaustive?  Well, we want to say yes.  And with the existing 
null-hostility of switch, it is.  But even without that, we’d like to 
say yes, because a null enum value is almost always an error, and making 
users deal with cases that don’t happen in reality is kind of rude.

For a domain sealed to a set of alternatives (enums or sealed classes), 
let’s say that a set of patterns is _weakly exhaustive_ if it covers all 
the alternatives but not null, and _strongly exhaustive_ if it also 
covers null.  When we did switch expressions, we said that weakly 
exhaustive coverings didn’t need a default in a switch expression.  I 
think we’re primed to say the same thing for sealed classes.  But, this 
“weak is good enough” leans on the fact that the existing hostility of 
switch will cover what we miss.  We get no such cover in nested cases.

I think it’s worth examining further why we are willing to accept the 
weak coverage with enums.  Is it really that we’re willing to assume 
that enums just should never be null?  If we had type cardinalities in 
the language, would we treat `enum X` as declaring a cardinality-1 type 
called X?  I think we might.  OK, what about sealed classes?  Would the 
same thing carry over?  Not so sure there.  And this is a problem, 
because we ultimately want:

     case Optional.of(var x):
     case Optional.empty():

to be exhaustive on Optional<T>, and said exhaustiveness will likely 
lean on some sort of sealing.

This is related to Guy's observation that totality is a "subtree all the 
way down" property.  Consider:

     sealed class Container<T> permits Box, Bag { }
     sealed class Shape permits Rect, Circle { }

Ignoring null, Box+Bag should be exhaustive on container, and 
Rect+Circle should be exhaustive on shape.  So if we are switching over 
a Container<Shape>, then what of:

     case Box(Rect r):
     case Box(Circle c):
     case Bag(Rect r):
     case Bag(Circle c):

We have some "nullity holes" in three places: Box(null), Bag(null), and 
null itself.   Is this set of cases exhaustive on Bags, Boxes, or 
Containers?

I think users would like to be able to write the above four cases and 
treat it as exhaustive; having to explicitly provide Box(null) / Box b, 
Bag(null) / Bag b, or a catch-all to accept null+Box(null)+Bag(null) 
would all be deemed unpleasant ceremony.

Hmm...

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200814/f75f80cb/attachment-0001.htm>