[pattern-switch] Opting into totality

[Brian Goetz]

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.

> 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.


(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.)

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.  So should it be 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.

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.







On 8/31/2020 11:17 AM, Remi Forax wrote:
>
>
> ------------------------------------------------------------------------
>
>     *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: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
>         <brian.goetz at oracle.com <mailto: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/c1443e56/attachment-0001.htm>