[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é: Vendredi 4 Septembre 2020 23:51:54
> Objet: Re: [pattern-switch] Opting into totality

> Let me add another option to the menu. I'm not sure I like it, but it's less bad
> than many of the alternatives suggested, and not incompatible (but has a more
> complex compatibility boundary), so worth putting on the table.

> Remi suggested:

> > say that (statement and expression) arrow switches are always total.

> Coupling this to arrow switches only was definitely the wrong axis on which to
> cut this, but there might be another that isn't so bad: say that switches over
> types other than { primitives, boxes, strings, enums } are always total, and we
> ask users to totalize otherwise-partial switches with `default: <something or
> nothing>`. Alternately, we could couple this not to the type, but to switches
> with _any non-constant cases_. (This seems better than keying off of the type.)

yes, any non-constant cases is better partitioning than switch on types. 
I believe the same partitioning/divider can be use for the nullable/non-nullable switch, i.e. a switch with only constant cases (and an optional default) reject null, all the others are nullable. 

> Then we can optionally combine it with the (not so good) idea in the previous
> mail -- implicit remainder handling -- which becomes a better idea in this
> context, since it only comes into play when an optimistically total but not
> strongly total set of cases is present.

> So we have { expression, statement } x { arrow, colon } switches, and the
> totality rules are: a switch is total if it is an expression switch, or it has
> any non-constant patterns. Total switches then get an implicit throwing default
> if they have no strongly total pattern. That's a kind of irregular shape, but
> possibly justifiable.

> I'm not sure I like it, because I am not yet convinced that partial pattern
> statement switches won't be common, but I'll have to think about it. It is
> definitely a bigger mental shift for users about what switch means.

I think i still prefer an explicit keyword at the end of the statement switch, let's call it "no-default", 
semantically equivalent to 
case var x: 
if (x == null) throw null; // if x is nullable, so not for primitive and inline in the future 
throw new ICCE(); 
but the compiler checks that the switch without "no-default" is optimistically total. 

so 
switch(shape) { 
case Circle: ... 
case Rect: ... 
no-default; 
} 
is total. 

and 
switch(object) { 
case Foo: 
default: ... 
no-default; 
} 
is not valid because no-default is not reachable. 

And if we keep the idea that a switch with a least a non-constant case has to be total, no-default is invalid in a switch expression and in a switch with a non-constant case. 

Rémi 

> On 9/3/2020 2:16 PM, Brian Goetz wrote:

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

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

>> So, I think we got it right then; we just have some holes to patch.

>> 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/20200906/fb5e39ea/attachment.htm>