[pattern-switch] Opting into totality
Brian Goetz
brian.goetz at oracle.com
Thu Sep 3 19:37:56 UTC 2020
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>
More information about the amber-spec-experts
mailing list