----- Mail original -----
> De: "Maurizio Cimadamore" <maurizio.cimadam...@oracle.com>
> À: "Brian Goetz" <brian.go...@oracle.com>, "Remi Forax" <fo...@univ-mlv.fr>
> Cc: "amber-spec-experts" <amber-spec-experts@openjdk.java.net>
> Envoyé: Mercredi 28 Avril 2021 18:33:53
> Objet: Re: Switch labels (null again), some tweaking
> On 28/04/2021 17:29, Brian Goetz wrote:
>> I assume that you are saying Box permits Soup only. But your
>> assumptions about "where do the nulls go" here are not right.
>> Box(Soup) does not match Box(null); the set of patterns { Box(Soup) }
>> is total on Box(Lunch) _with remainder Box(null)_. So the null paths
>> in this example are dead. (Also missing break statements.) So
>> rewriting, this switch is really equivalent to:
>>
>> switch (lunch) {
>> case Box(Soup s):
>> System.err.println("Box of soup");
>> break;
>>
>> case Bag(Soup s):
>> System.err.println("Bag of soup");
>> break;
>>
>> /* implicit */
>> case Box(null), Bag(null): throw new NPE();
>> }
>>
>> and the switch is total on Container(Lunch) under the Lunch=Soup,
>> Container=Box|Bag assumptions.
>
> I have to admit that this is surprising.
>
> So, if I have a sealed hierarchy that only permits one concrete type:
>
> interface Foo permits Bar
>
> doing:
>
> Foo x = ...
> if (x instanceof Bar)
>
> is not considered a total instanceof?
There is no notion of totality for instanceof.
For a switch, the concept of totality exist because when you have a switch you
have two ways of seeing a switch as a cascade of "if ... instanceof".
The question is should the last case be the equivament of "else", or not ?
By example,
switch(x) {
case Foo foo:
case Bar bar:
}
can be seen either as
if (x instanceof Foo foo) { ... }
if (x instanceof Bar bar) { ... }
or
if (x instanceof Foo foo) {
...
} else {
...
}
If x is declared as a Bar, then "case Bar bar" is total, so the later
translation/semantics is used,
if Foo and Bar are subtypes of a sealed type, "case Bar bar" is not total, the
former semantics is used.
And as Brian said, it also works the same way with sub-patterns i.e. it
composes well.
>
> Maurizio
Rémi
