[pattern-switch] Opting into totality

[Brian Goetz]

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

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.



On 9/3/2020 3:30 PM, forax at univ-mlv.fr wrote:
>
>
> ------------------------------------------------------------------------
>
>     *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" <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/20200903/4e2b24c5/attachment.htm>