[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 21:37:56
> Objet: Re: [pattern-switch] Opting into totality

> We knew at the time we were might want to come back for totality of switches --
> not as "fixing a mistake", but providing more type checking when the user asks
> for it. So I don't think any of the "but now we realize it is different"
> applies, nor do I see any new evidence that somehow we missed something
> substantial then. (I recall you wanted to do a more aggressive "fix mistakes of
> the past" option at the time; I think this is mostly taking a second swing
> along those lines.)
It's not exactly fixing the mistakes of the past and more wanting to be able to refactor a switch expression to a switch statement back and forth without thinking too much if i recall correctly. 

> Note that we still have the alternative to do nothing: let the user be on their
> own with totality for statement switches. That wasn't a terrible option in 12
> (which is why we pushed it off until now), and it's still not really terrible
> now; it's just that the number of cases of nontrivial totality, and the
> complexity of the remainder, has gone up and will go up more in the future
> (enums yesterday; sealed types today; deconstruction patterns tomorrow), which
> provides some additional pressure for a "total statement switch" option. Which
> we could do now, or later, or never.
yes, doing nothing is an option, but it means giving up on having an error reported by the compiler in a switch statement when you add a new subtypes to a sealed types, which is a kind of sad. 

Rémi 

> On 9/3/2020 3:30 PM, [ mailto:forax at univ-mlv.fr | forax at univ-mlv.fr ] wrote:

>>> De: "Brian Goetz" [ mailto:brian.goetz at oracle.com | <brian.goetz at oracle.com> ]
>>> À: "Remi Forax" [ mailto:forax at univ-mlv.fr | <forax at univ-mlv.fr> ]
>>> Cc: "amber-spec-experts" [ mailto:amber-spec-experts at openjdk.java.net |
>>> <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/598684ec/attachment-0001.htm>