[pattern-switch] Totality

[Brian Goetz]

On 8/21/2020 11:14 AM, Brian Goetz wrote:
>
> Next up (separate topic): letting statement switches opt into totality.
>

Assuming the discussion on Exhaustiveness is good, let's talk about 
totality.

Expression switches must be total; we totalize them by throwing when we 
encounter any residue, even though we only require that the set of cases 
in the switch be optimistically total.  Residue includes:

  - `null` switch targets in String, Enum, and primitive box switches only;
  - novel values in enum switches without a total case clause;
  - novel subtypes in switches on sealed types without a total case clause;
  - when an optimistically total subchain of deconstruction pattern 
cases wraps a residue value (e.g., D(null) or D(novel))

What about statement switches?  Right now, any residue for a statement 
switch without a total case clause will just be silently ignored 
(because statement switches need not be total.)

What we would like is a way to say "this switch is total, please type 
check it for me as such, and insert any needed residue-catching cases."  
I think this is a job for `default`.

Now that we've got some clarity that switches _don't_ throw on null, but 
instead it is as if string/enum/box switches have an implicit `case 
null` when no explicit one is present, we can define `default`, once 
again, to be total (and not just weakly total.)  So in:

     switch (object) {
         case "foo":
         case Box(Frog fs):
         default: ...
     }

a `null` just falls into `default` just like anything else that is not 
the string "foo" or a box of frogs ("let the nulls flow"). Default would 
have to come last (except in legacy switches, where a legacy switch has 
one of the distinguished target types and all constant case labels.)

What if we want to destructure too?  Well, add a pattern:

     switch (object) {
         case "foo":
         case Box(Frog fs):
         default Object o: ...
     }

This would additionally assert that the following pattern is total, 
otherwise a compilation error ensues.  (Note, though, that this is 
entirely about `switch`, not patterns.  The semantics of the pattern is 
unchanged, and I do not believe that sprinkling `default` into nested 
patterns to shout "TOTALITY HERE, I MEAN IT" carries its weight.)

This seems a better job to give default in this new world; anything not 
previously matched, where we retcon the current null behavior as being 
only about string, enum, or boxes.

This leaves us with only one hole, which is: suppose I have an 
_optimistically total_ statement switch.   Users might like to (a) 
assert the switch is total, and get the concomitant type checking, and 
(b) get residue ejection for free.  Of the two, though, A is much more 
important than B, but we'll take B when we can get it. Perhaps, if the 
target of a switch is a sealed type, we can interpret:

     switch (shape) {
         case Rect r: ...
         default Circle c: ...
     }

as meaning that `Circle c` _closes_ the switch to make it total, and 
engages the totality checking to ensure this is true.  So, `default P` 
would mean either:

  - P is total, or
  - P is not total, but taken with the other cases, makes the switch 
optimistically total

and in the latter case, would engage the residue-detection-and-ejection 
machinery.

This might be stretching it a tad too far, but I like that we can given 
`default` useful new jobs to do in `switch` rather than just giving him 
a gold watch.