[pattern-switch] Opting into totality

[forax at univ-mlv.fr]

> De: "Brian Goetz" <brian.goetz at oracle.com>
> À: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Jeudi 3 Septembre 2020 20:16:10
> Objet: Re: [pattern-switch] Opting into totality

> 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.
yes, that made sense at the time, the problem is that now we want seom statement switches to be total. 

> 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.
It's not random, arrow switch avoid fallthrough in between cases but weirdly allow a to fallthrough the whole switch. 
So it's not about having the semantics right, it's about making the semantics consistent, here the story being able to fall to the next instruction is not consistent. 

> 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.
Very true, but now you are saying that you want to introduce an opt-in to totality for the switch statement, so it's not orthogonal anymore. 

> 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.
The fact that you can implicitly skip the whole switch with arrows it's a complex control flow, , so that part is not fully orthogonal too. 

> So, I think we got it right then; we just have some holes to patch.
The problem is that introducing a switch statement that requires totality goes full throttle against the idea that a statement switch implies partiallity. 

Rémi 

> 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" [ mailto:brian.goetz at oracle.com | <brian.goetz at oracle.com> ]
>>> À: "amber-spec-experts" [ mailto:amber-spec-experts at openjdk.java.net |
>>> <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/20200903/2fe5447e/attachment.htm>