[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é: Lundi 31 Août 2020 17:51:54
> Objet: Re: [pattern-switch] Opting into totality

> What you're suggesting is that we should treat statement switch partiality as a
> legacy behavior of existing switches on { primitives, boxes, strings, and enums
> }, and then say the rest of the switches are total. (I must observe that the
> irony that you'd raise the spectre of "snitch" and then in the same breath make
> a proposal like this is pretty "total".)

> Not only is this a far more intrusive change, but it also ignores something
> fundamental: partiality for statement switches _is a feature, not a bug_. A
> partial switch is like an `if` without an `else`; no one thinks such things are
> mistakes, and a rule that required an `else` on every `if` would not be
> appreciated. I appreciate the attempt at symmetry, and all things being equal
> that would be nice, but I don't think all things are equal here. I think this
> asks far too much of users to stretch their mental model in this way -- nor do
> I think it is worth the benefit, nor am I even convinced we'd actually even
> achieve the benefit in practice.
'if' and 'switch' are dual, 'if' is oriented toward doing one test on a value and 'switch' is oriented to doing several tests on the same value. 
So a partial switch is not like an 'if', it's like a cascade of 'if/else' so forcing to have an 'else' when you have a cascade of 'if/else' seems not as bad as your are suggesting. 

Yes, it's a more intrusive change but it using the playbook on how to grow a language, to avoid to add features on top of features to the point the language is too hard to understand, the idea is that when you add a feature, you do that in a way that retrofit an existing feature so the number of features stay more or less constant. 

I don't think that a partial statement is a bug. The rules i propose make it more explicit by adding "default:" or "default -> {}" at the end, but the semantics is still the same. 

>> for 1/, it's about designing with the future in mind, if most switch are switch
>> on types, let have the right behavior
> I think you lost me already, as I don't think it's the right behavior.
> Statements are partial.
Ok, here i should have use "right default" instead of "right behavior", you are right that it's not about the behavior, my bad on that. 

> (I probably shouldn't even mention that this creates a new "action at a
> distance" problem since the totality semantics depend on the operand type (see,
> I was on the debate team in high school too), so I won't, because it would be
> unconstructive.)
good you did not mention it because as far as i understand for null, there is a difference between a switch on types and the already existing switches. 

> But I will mention that the operand type isn't even the right thing to key off
> of here, because even if we are switching on strings, we might still want to
> use type patterns with guards:

> switch (int) {
> case 0: println("zero");
> case 1: println("one");
> case int x where x%2 == 0: println("even");
> }

> Is this an old switch, or a "type" switch? Well, it can't be expressed as an old
> switch, since it uses type patterns, but it is a switch on old types.
Good question, 
from the user POV it's either an error or a warning, so in both cases it's a call for action, so for most user, using Alt+Enter or Ctrl+1 will fix the issue (insert a "default:") 
for us the EG or people writing compilers, it's a new switch because you have a case that is using a pattern. 

> So should it be total?
If you get an error or a warning it's because it's not total. 

> I think the line where you want to cut is fuzzier than you think, and that's
> going to confuse the heck out of users.
The new switch will confuse a lot of users anyway, it's something i have remarked when doing presentations about the pattern matching, you have to explain the syntax because not enough Java devs have not been exposed to pattern matching in an another languages before. 
So 

> So overall, while it's a fair question to ask "could we get away with defining
> switch to always be total, carve out an exception for all the existing idioms,
> and not confuse the users too much", I think that would be taking it too far.
I think that retrofitting the old switch to a common behavior at the same time you introduce the new construct is not too far, again as you said during the development of the expression switch, it's far easier to explain one behavior that to explain multiple (statement vs expression switch with respect to totality) or to have to explain when to use which kind of switch (switch vs sealed-switch). 

Rémi 

> On 8/31/2020 11:17 AM, Remi Forax wrote:

>>> 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:35:32
>>> Objet: Re: [pattern-switch] Opting into totality

>>> Totality is a term that language designers like, but may not be all that
>>> evocative to users. So switch-total might not exactly turn on the light bulb
>>> for them. In this manner, “sealed” has a useful connotation that has nothing to
>>> do with sealed types: non-leakiness: a sealed switch doesn’t leak any
>>> unprocessed values!

>>> Test driving ...

>>> sealed switch (x) { … }
>>> sealed-switch (x) { … }
>>> switch-sealed (x) { … }

>>> “A switch may be sealed with the sealed modifier; expression switches are
>>> implicitly sealed. The set of case patterns for a sealed switch must be total
>>> with some remainder; synthetic throwing cases are inserted for the remainder.”

>> Those are all "snitch" moves, let's avoid that because all you said about having
>> more than one kind of switch still apply.

>> Here are some facts that can help us,
>> - there is not a lot of existing switches in the wild
>> - as you said, there is a very good chance that the switch on types become the
>> dominant switch.

>> Now, divide and conquer,
>> 1/ a switch on type (statement or expression) should always be non leaky
>> 2a/ add a warning on all existing leaky statement switches forcing them to have
>> a default if not exhaustive
>> 2b/ for an exhaustive enum switch, add a warning if the switch has a default.
>> and if there is no default, let the compiler add a "default -> throw ICCE", it's
>> a breaking change but it should be ok because IDEs currently ask for a default
>> in a switch on enums.
>> explanations
>> for 1/, it's about designing with the future in mind, if most switch are switch
>> on types, let have the right behavior
>> for 2a/, ask users to fix leaky statement switches, even if we introduce a
>> selaed-switch, we will need this warning to gradually move to a better world.
>> for 2b/, ask users to fix exhaustive enum switches so it works like a switch on
>> type.

>> I may be wrong with the idea of adding a "default -> throw" on enum switches
>> without a default, it may break a lot of codes, but i believe it worth the try.

>> And BTW, we should also emit a warning if the default is in the middle of the
>> switch, again to drive user to think in term of switch on type constraints.

>> Rémi

>>>> On Aug 31, 2020, at 9:25 AM, Brian Goetz < [ mailto:brian.goetz at oracle.com |
>>>> brian.goetz at oracle.com ] > wrote:

>>>> 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/20200831/687b89ba/attachment-0001.htm>