Opting into totality

[Guy Steele]

See below and also far below.

> On Aug 24, 2020, at 7:06 PM, Guy Steele <guy.steele at oracle.com> wrote:
> 
> More later (I have a meeting soon), but for now, remember that customized residue handling can _always_ be handled with a case label (such as “case var x”, or something more specific); you don’t need “default”. 
> 
> Sent from my iPhone

Indeed, to me much of the value of the residue model lies in demonstrating that the residue can be characterized in terms of additional synthesized switch labels, and that the user can therefore easily supersede any such synthesized label by providing it explicitly.

>> On Aug 24, 2020, at 6:17 PM, Brian Goetz <brian.goetz at oracle.com> wrote:
>> 
>> 
>>>> One question I have is that optimistic totality can apply in switches that are not on sealed types, or where sealed types show up in nested contexts.  For example:
>>>> 
>>>>    switch (box) {
>>>>        case Box(var x): ...
>>>>    }
>>>> 
>>>> Here, I think we want to say that Box(var x) is o.t. on Box, but it doesn't match null.   So how does the programmer indicate that they want to get totality checking and residue rejection?
>>> I believe that “switch case” can handle this:
>>> 
>>>    switch case (box) {
>>>        case Box(var x): ...
>>>    }
>>> 
>>> This says, among other things, that it is a static error if the (singleton) set of case patterns { Box(var x) } is not o.t. on the type of “box”, and it says we want residue checking, so it’s as if the compiler rewrote it to:
>>> 
>>>    switch case (box) {
>>>   case null: throw <null residue error, which could be NPE or something else>
>>>        case Box(var x): ...
>>>    }
>>> 
>>> Alternatively, we could write
>>> 
>>>    switch (box) {
>>>        default Box(var x): ...
>>>    }
>>> 
>>> which says that it is a static error if the pattern Box(var x) is not total on the type of “box”.  It’s not, because it doesn’t match null, so we get a static error, as desired.  Perhaps we should have written
>>> 
>>>    switch (box) {
>>>        case Box(var x): …
>>>   default Box z: ...
>>>    }
>>> 
>>> But I’m thinking the “switch case” solution is preferable for this specific example.
>> 
>> OK, so (taking this example with the next) the mental model for `switch case` is not as I suggested -- "switch by covering parts" -- as much as "a switch that is optimistically total, and which gets built-in residue rejection."  Because there are multiple categories of o.t. that don't involve enum/sealed types at all, or that get their optimism only indirectly through enum/sealed types.
>> 
>> Let me probe at another aspect; that it is an error for a `switch case` to have a default clause.  This seems a tad on the pedantic side, in that surely if you add a `default` clause to an already o.t. switch with non-empty residue, it is (a) still total and (b) might afford you the opportunity to customize the residue rejection.  But I think your response would be "that's fine, it's not a switch case, it's an ordinary total switch with a default clause.
>> 
>> Which says to me that you are motivated to highlight the negative space between "optimistically total" and "total"; what a `switch case` asserts is _both_ that the set of cases is optimistically total, _and_ that there's a non-empty residue for which which we cede responsibility to the switch.  (Secondarily, I think you're saying that a `default` at the end of the switch is enough to say "obviously, it's total.")

I have thought about what you have just said; (a) I agree, and (b) have made me realize that I have unnecessarily and unreasonably conflated the o.t. issue with the fallthrough issue.  So let me try once more.  For context, here are the three important paragraphs again, and the only changes I have made are to remove from the third paragraph the sentences that address fallthrough and fallout:

—————————————
Then we introduce two mechanisms that we have discussed more recently, and say that each of these mechanisms may be used in either a switch statement or a switch expression.

The first is a switch label of the form “default <pattern>”, which behaves just like a switch label “case <pattern>” except that it is a static error if the <pattern> is not total on the type of the selector expression.  This mechanism is good for extensible type hierarchies, where we expect to call out a number of special cases and then have a catch-all case, and we want the compiler to confirm to us on every compilation that the catch-all case actually does catch everything.

The second is the possibility of writing “switch case” rather than “switch”, which introduces these extra constraints on the switch block: It is a static error if any SwitchLabel of the switch statement begins with “default".  It is a static error if the set of case patterns is not at least optimistically total on the type of the selector expression.  In addition, the compiler automatically inserts SwitchBlockStatementGroups or SwitchRules to cover the residue, so as to throw an appropriate error at run time if the value produced by the selector expression belongs to the residue.  This mechanism is good for enums and sealed types, that is, situations where we expect to enumerate all the special cases explicitly and want to be notified by the compiler (or failing that, at run time) if we have failed to do so.
—————————————

I also considered removing the sentence

    It is a static error if any SwitchLabel of the switch statement begins with “default”.

which is the one that makes these two options mutually exclusive.  But under this slimmed-down definition, if you add a “default” clause to a “switch case” construct, then the fact that you used “switch case” has no effect: the “default” clause ensures that the set of patterns is total, therefore also o.t., and the residue will be empty.  So there is no point is allowing both features to be used together.

Now we have twelve combinations produced by three orthogonal choices:

	statement or expression

	there is a single pattern that must be total (“default”), or the set of patterns must be o.t. (“switch case”), or no totality constraint

	fallthrough could happen (switch blocks using colons) or cannot happen (switch rules using ->)

and two of them have additional rules to ensure that a switch expression need not generate default values.