[pattern-switch] Totality

[forax at univ-mlv.fr]

> De: "Guy Steele" <guy.steele at oracle.com>
> À: "Brian Goetz" <brian.goetz at oracle.com>
> Cc: "Remi Forax" <forax at univ-mlv.fr>, "Tagir Valeev" <amaembo at gmail.com>,
> "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Samedi 22 Août 2020 02:32:13
> Objet: Re: [pattern-switch] Totality

>> On Aug 21, 2020, at 4:18 PM, Brian Goetz < [ mailto:brian.goetz at oracle.com |
>> brian.goetz at oracle.com ] > wrote:

>> On 8/21/2020 11:14 AM, Brian Goetz wrote:

>>> Next up (separate topic): letting statement switches opt into totality.

>> Assuming the discussion on Exhaustiveness is good, let's talk about totality.

>> Expression switches must be total; we totalize them by throwing when we
>> encounter any residue, even though we only require that the set of cases in the
>> switch be optimistically total. Residue includes:

>> - `null` switch targets in String, Enum, and primitive box switches only;
>> - novel values in enum switches without a total case clause;
>> - novel subtypes in switches on sealed types without a total case clause;
>> - when an optimistically total subchain of deconstruction pattern cases wraps a
>> residue value (e.g., D(null) or D(novel))

>> What about statement switches? Right now, any residue for a statement switch
>> without a total case clause will just be silently ignored (because statement
>> switches need not be total.)

>> What we would like is a way to say "this switch is total, please type check it
>> for me as such, and insert any needed residue-catching cases." I think this is
>> a job for `default`.

>> Now that we've got some clarity that switches _don't_ throw on null, but instead
>> it is as if string/enum/box switches have an implicit `case null` when no
>> explicit one is present, we can define `default`, once again, to be total (and
>> not just weakly total.) So in:

>> switch (object) {
>> case "foo":
>> case Box(Frog fs):
>> default: ...
>> }

>> a `null` just falls into `default` just like anything else that is not the
>> string "foo" or a box of frogs ("let the nulls flow"). Default would have to
>> come last (except in legacy switches, where a legacy switch has one of the
>> distinguished target types and all constant case labels.)

>> What if we want to destructure too? Well, add a pattern:

>> switch (object) {
>> case "foo":
>> case Box(Frog fs):
>> default Object o: ...
>> }

>> This would additionally assert that the following pattern is total, otherwise a
>> compilation error ensues. (Note, though, that this is entirely about `switch`,
>> not patterns. The semantics of the pattern is unchanged, and I do not believe
>> that sprinkling `default` into nested patterns to shout "TOTALITY HERE, I MEAN
>> IT" carries its weight.)

>> This seems a better job to give default in this new world; anything not
>> previously matched, where we retcon the current null behavior as being only
>> about string, enum, or boxes.

>> This leaves us with only one hole, which is: suppose I have an _optimistically
>> total_ statement switch. Users might like to (a) assert the switch is total,
>> and get the concomitant type checking, and (b) get residue ejection for free.
>> Of the two, though, A is much more important than B, but we'll take B when we
>> can get it. Perhaps, if the target of a switch is a sealed type, we can
>> interpret:

>> switch (shape) {
>> case Rect r: ...
>> default Circle c: ...
>> }

>> as meaning that `Circle c` _closes_ the switch to make it total, and engages the
>> totality checking to ensure this is true. So, `default P` would mean either:

>> - P is total, or
>> - P is not total, but taken with the other cases, makes the switch
>> optimistically total

>> and in the latter case, would engage the residue-detection-and-ejection
>> machinery.

>> This might be stretching it a tad too far, but I like that we can given
>> `default` useful new jobs to do in `switch` rather than just giving him a gold
>> watch.

> This is a pretty good story, but I am sufficiently distressed over the asymmetry
> of having to treat specially the last one of several otherwise completely
> symmetric and equal cases:

> switch (color) {
> case Red: …
> case Green: …
> default Blue: …
> }

> when I would much rather see

> switch (color) {
> case Red: …
> case Green: …
> case Blue: …
> }

> that I am going to explore several other design options, some of them more
> obviously terrible than others, in hopes of prompting someone else to have a
> brilliant idea.

> First of all, let me note that after Brian’s detailed analysis about the
> treatment of `null`, the only real difficulty we face is compatibility with
> legacy switches on enum types. We missed an opportunity when enum was first
> introduced. I really hate to recommend an incompatible change to the language,
> but this message is just brainstorming, so:

> Option 1: If the type of the switch expression is an enum or a sealed type, then
> it is a static error if the patterns are not at least optimistically total.
> **This would be an incompatible change with respect to existing switches on
> enum types.**

> Option 2: If the type of the switch expression is a sealed type, then it is a
> static error if the patterns are not at least optimistically total. This treats
> enums and sealed types differently, but is compatible (as are all the other
> options I will list below).

> Option 3: If the type of the switch expression is a sealed type, then it is a
> static error if the patterns are not at least optimistically total. You can get
> the benefit of this feature when switching on an enum type by adding the
> keyword “sealed” to the declaration of the enum type.

> enum Color { RED, GREEN }
> Color x;
> switch (x) { RED: … }// Okay

> sealed enum Color { RED, GREEN }
> Color x;
> switch (x) { RED: … }// static error: cases are not optimistically total

> Option 4: If the type of the switch expression is a sealed type, then it is a
> static error if the patterns are not at least optimistically total. You can get
> the benefit of this feature when switching on an enum type by adding the
> keyword “enum” to the switch statement.

> enum Color { RED, GREEN }
> Color x;
> switch (x) { RED: … }// Okay

> enum Color { RED, GREEN }
> Color x;
> switch enum (x) { RED: … }// static error: cases are not optimistically total

> Option 5: Expression switches must be total. So if you want a statement switch
> but want it to be total, convert it to an expression switch by writing “(void)”
> in front of it (and add a semicolon at the end).

> enum Color { RED, GREEN }
> Color x;
> switch (x) { RED: … }// Okay

> enum Color { RED, GREEN }
> Color x;
> (void) switch (x) { RED: … };// static error: cases are not optimistically total

> (Yeah, I have glossed over a number of details here.)

I've already written a code organically doing mostly that, transforming a statement switch to an expression switch to be sure it did not compile when i will add more enum constants, 
var _ = switch(x) { 
case RED: 
... 
yield false; 
case GREEN: 
... 
yield false 
}; 

> Option 6: The classic idiom for switching on a enum type looks like this example
> taken from the JLS:

> switch (c) {
> case PENNY: return CoinColor.COPPER;
> case NICKEL: return CoinColor.NICKEL;
> case DIME: case QUARTER: return CoinColor.SILVER;
> default: throw new AssertionError("Unknown coin: " + c);
> }

> The only really annoying thing about this is having to write (and read) the
> boilerplate code for constructing the error to be thrown. So how about this
> abbreviation:

> switch (c) {
> case PENNY: return CoinColor.COPPER;
> case NICKEL: return CoinColor.NICKEL;
> case DIME: case QUARTER: return CoinColor.SILVER;
> default throw;
> }

> The meaning of “default throw;” is that it is a static error if the case
> patterns are not optimistically total (and it reminds you that you will get
> some synthetic default cases that will throw an error if something goes wrong).

If we go down to the route of saying that switch on enum, string and box are special because null hostile, 
why not go a step further and say that, apart those switches and the switch one primitive types, all other switches should be total, so obviously an expression switch should be total but a statement switch should be total too. 

And now we only need to solve the problem of enums inside a statement switch, here i disagree with Brian that it's a job for "default", as a developer i want the compiler to emit an error at compile time not at runtime. 
I wonder if like Option 1 we can not bully our way out by first raising a warning if the statement switch is not optimistically total (IDEs already does that but ask for a default) and adds an ICCE automatically if the switch is total (it's a behavior incompatible change but it's for aligning the statement switch to the expression switch and i believe it will be fine in real life) then later convert that warning to an error like we want to do with wrapper type and ==. 

I also want to add that if we add things like guards, we may also want this kind of switches to be exhaustive, 
int i = ... 
switch(i) { 
case i where i > 0: ... 
} 

Rémi 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200822/82eac058/attachment-0001.htm>