[pattern-switch] Opting into totality

[Brian Goetz]

Another alternative that I'll put in for the record, but which is 
brittle, is:

  - If the set of patterns of a statement switch is total with nonempty 
remainder R, insert a throwing default for R.

This means that in

     switch (box) {
         case Box(var x): ...
     }

which is total on Box with remainder { null }, we'd get an NPE on a null 
box.  Essentially, we infer totality for statement switches, and 
remainder-rejection comes with the totality.

The brittleness comes from the fact that, if you miss a case of a sealed 
type, not only do you not find out your switch isn't total any more, but 
your remainder rejection goes away.  I don't like it, but this reframing 
might point to a slightly different way to say "I'm assuming totality, 
tell me if I'm wrong."

On 9/4/2020 2:06 PM, Brian Goetz wrote:
>
>> I bring this up again not to defend the syntax, but to underscore a 
>> more important point: that we thought at first that “sealing” 
>> switches was about asserting totality and enlisting the compiler’s 
>> aid in verifying same, but as we worked through the cases, and 
>> discovered there were more cases of remainder than we initially 
>> thought, the main value of sealing instead became restoring the 
>> switch to having no unhandled remainder.  Whatever syntax we choose 
>> should try to evoke that at least as much as evoking totality of the 
>> case labels. 
>
> Taking this a little further: it is not that interesting to declare a 
> switch `sealed` that has a default clause or other total pattern; such 
> switches are "obviously" total and non-leaky.  It's nice, but we 
> wouldn't add a language feature for it.
>
> The interesting part of sealing a switch are cases like this. Assume 
> Shape = Circ | Rect.
>
>     switch (shape) {
>         case Circ c:
>         case Rect r:
>     }
>
> Here, sealing gives us two things: asserting we've covered all the 
> cases (which is not going to be obvious except in the most trivial of 
> sealed types) and handling of remainder (here, only null.) Similarly:
>
>     switch (boxOfShape) {
>         case Box(Circ c):
>         case Box(Rect r):
>     }
>
> Same basic story -- not obvious that we've covered all boxes, the 
> remainder is just slightly more complicated.
>
> The compile-time checking for optimistic totality, and runtime 
> checking for remainder, are two sides of the same coin; we are stating 
> expectations that all possible inputs are covered, either by an 
> explicit case or by an implicit remainder case.  We statically check 
> the ones we can, and dynamically reject the "acceptable 
> non-coverage."  (Characterizing the acceptable non-coverage is the 
> main bit of positive progress we've made recently.)
>
> I think we may be skipping over a step by jumping to "throwing syntax 
> at the problem."  The real question is, what do we want the users 
> thinking about when they are coding, and what should we not be 
> bothering them with?  We've already acknowledged that we _don't_ want 
> them worrying about explicitly managing the remainder.
>
> We've been approaching this as "I assert that this switch is 
> sufficiently total", which included both strongly total and 
> optimistically total switches (because that's what we already do for 
> expression switches.)  But given that having a default case makes it 
> obviously total (and obviates the need for remainder handling), 
> perhaps we want to focus on the user asserting "I know I didn't write 
> a default, but I am still covering all the cases." Does that offer a 
> different enough viewpoint that other options come into focus?