[pattern-switch] Opting into totality

[Brian Goetz]

Let me add another option to the menu.  I'm not sure I like it, but it's 
less bad than many of the alternatives suggested, and not incompatible 
(but has a more complex compatibility boundary), so worth putting on the 
table.

Remi suggested:

 > say that (statement and expression) arrow switches are always total.

Coupling this to arrow switches only was definitely the wrong axis on 
which to cut this, but there might be another that isn't so bad: say 
that switches over types other than { primitives, boxes, strings, enums 
} are always total, and we ask users to totalize otherwise-partial 
switches with `default: <something or nothing>`.  Alternately, we could 
couple this not to the type, but to switches with _any non-constant 
cases_.  (This seems better than keying off of the type.)

Then we can optionally combine it with the (not so good) idea in the 
previous mail -- implicit remainder handling -- which becomes a better 
idea in this context, since it only comes into play when an 
optimistically total but not strongly total set of cases is present.

So we have { expression, statement } x { arrow, colon } switches, and 
the totality rules are: a switch is total if it is an expression switch, 
or it has any non-constant patterns.  Total switches then get an 
implicit throwing default if they have no strongly total pattern.  
That's a kind of irregular shape, but possibly justifiable.

I'm not sure I like it, because I am not yet convinced that partial 
pattern statement switches  won't be common, but I'll have to think 
about it.  It is definitely a bigger mental shift for users about what 
switch means.






On 9/3/2020 2:16 PM, Brian Goetz wrote:
> That came up in the expression switch exploration.  The thinking then, 
> which I think is still valid, that it is easier to understand the 
> difference when default-totality is attached to the expression 
> versions, because expressions _must_ be total and statements totally 
> make sense to be partial.
>
> I think this is still coming from a place of retrospective 
> snitch-envy; you want to carve out a corner that has the "right" 
> semantics, even if its relation to the other corners is totally ad-hoc 
> and random.  The upgrade to switch was driven by orthogonality; 
> totality derives from whether the context of the switch (statement vs 
> expression) requires totality or embraces partiality.  And the kinds 
> of labels are strictly about the treatment of what is on the RHS -- 
> either a single { expression/statement } vs complex control flow. 
> Which is orthogonal to expression/statement.
>
> So, I think we got it right then; we just have some holes to patch.
>
> On 9/3/2020 1:04 PM, Remi Forax wrote:
>> I just want to say that the is yet another option,
>> say that (statement and expression) arrow switches are always total.
>>
>> We have introduced the arrow notation to avoid fallthrough but we 
>> have forgotten one important case of fallthrough, in a statement 
>> switch when you skip the entire switch, you fallthrough the entire 
>> switch.
>>
>> So we keep supporting the traditional partial switch with no 
>> modification but requires if a user wants a partial arrow switch, to 
>> add a "default -> {}".
>>
>> This is an incompatible change with the codes written since Java 14 
>> so it's a limited incompatible change.
>> Perhaps the main blocker is admitting that we were wrong.
>>
>> Rémi
>>
>> ------------------------------------------------------------------------
>>
>>     *De: *"Brian Goetz" <brian.goetz at oracle.com>
>>     *À: *"amber-spec-experts" <amber-spec-experts at openjdk.java.net>
>>     *Envoyé: *Lundi 31 Août 2020 15:25:13
>>     *Objet: *Re: [pattern-switch] Opting into totality
>>
>>     I think this is the main open question at this point.
>>
>>     We now have a deeper understanding of what this means, and the
>>     shape of the remainder.  Totality means not only “spot check me
>>     that I’m right”, but also “I know there might be some remainder,
>>     please deal with it.”   So totality is not merely about type
>>     checking, but about affirmative handling of the remainder.
>>
>>     Expression switches automatically get  this treatment, and opting
>>     _out_ of that makes no sense for expression switches (expressions
>>     must be total), but statement switches make sense both ways (just
>>     like unbalanced and balanced if-else.)  Unfortunately the default
>>     has to be partial,  so the main question is, how  do we indicate
>>     the desire for totality in a way that is properly evocative for
>>     the user?
>>
>>     We’ve talked about modifying switch (sealed switch), a hyphenated
>>     keyword (total-switch), a trailing modifier (switch case), and
>>     synthetic cases (“default: unreachable”).  Of course at this
>>     point it’s “just syntax”, but I think our goal should be picking
>>     something that  makes it obvious to users that what’s going on is
>>     not merely an assertion of totality, but also a desire to handle
>>     the remainder.
>>
>>            - How does a switch opt into totality, other than by being
>>         an expression switch?
>>
>>
>>
>

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