Switch labels (null again), some tweaking

[forax at univ-mlv.fr]

----- Mail original -----
> De: "Maurizio Cimadamore" <maurizio.cimadamore at oracle.com>
> À: "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é: 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