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
> On Aug 24, 2020, at 6:17 PM, Brian Goetz <brian.go...@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.")
>
>
>
