Re: Switch labels (null again), some tweaking

[John Rose]

On Apr 29, 2021, at 8:19 AM, fo...@univ-mlv.fr wrote:

and let the runtime part bound to invokedynamic to take care of the remainder.

+100

and another +100 for the term-of-art “spiny”

Re: Switch labels (null again), some tweaking

[forax]

- Mail original -
> De: "Brian Goetz" 
> À: "Remi Forax" , "Maurizio Cimadamore" 
> 
> Cc: "amber-spec-experts" 
> Envoyé: Jeudi 29 Avril 2021 16:52:28
> Objet: Re: Switch labels (null again), some tweaking

> Without diving into the translation details prematurely, I just want to
> note that we *do* want the compiler to "totalize" things for us,
> because, DA.  Suppose we have A permits B, C:
> 
>     int x ;
>     switch (a) {
>     case B(int foo): x = foo; break;
>     case C(int bar): x = bar; break;
>     }
>     // HERE
> 
> There is some remainder -- null, D -- but we don't want that remainder
> to leak past the switch; when we get to HERE, we'd like x to be DA, and
> a to have matched one of the patterns.  So the compiler has to insert
> _something_ to handle the remaining cases, even if it is only:
> 
>     default: throw new TotalityException("blah blah");
> 

Not necessarily, the synthetic switch can use default for the last case

  int x;
  var carrier = invokedynamic (a);
  switch(carrier.dispatch) {
case 0:
  int foo = carrier.foo();
  x = foo;
  break;
default:
  int bar = carrier.bar();
  x = bar;
  break;
  } 

and let the runtime part bound to invokedynamic to take care of the remainder.  

> But, the details of code generation are not what M is asking about now
> -- he's asking "if I were the user, could I write a truly covering
> switch?"  And the answer is yes, but the shape of the remainder is
> "spiny" and can get complicated quickly.

Ok

Rémi

> 
>> Not necessarily.
>>
>> First, let's acknowledge that you are moving the discussion from the basic
>> semantics to talk about the translation strategy which touch more the binary
>> compatibility,
>> aka, what is the semantics when the view of the world at compile time and at
>> runtime are disagreeing.
>>
>> There are at least two reasons to let javac emits such cases,
>> first like with null as remainder, you have to add a lot of cases once you 
>> have
>> sub-patterns, so it will bloat the bytecode,
>> then if we insert such cases, it means that we also have a code that throw a
>> specific exception bolt into the bytecode which means that we can not change
>> the binary compatibility story later.
>>
>> The jobs to implement the binary compatibility semantics is the job of the
>> runtime not the compiler, like with lambdas, where the LambdaMetaFactory does
>> some runtime checks before generating + linking the lambda proxy,
>> I expect a SwitchMetafactory to do the same job. This is more flexible and
>> allows the runtime to be updated when the VM change by example, the
>> lambdaMetafactory code was changed with the introduction of hidden classes.
>>
>> Now, the big question is what binary compatibility semantics we want ?
>>
>> We can by example throw a subclass of LinkageError upfront during the linking
>> when we detect that the sealed type as more subclasses that the one 
>> accessible
>> at compile time, but it means that adding a new subclass to a sealed type is
>> not a binary compatible change anymore. We can delay the detection the an
>> incompatible class until we see one at runtime, so adding a new subclass is a
>> compatible change but calling a switch with an instance of such subclass is
>> not.
>>
>> There is also the question about the order of the cases, should the order of 
>> the
>> cases be validated at runtime or not, by example, if we have B < A at compile
>> time but A < B at runtime with a switch that like case B first and case A
>> second.
>>
>>> Maurizio
> > Rémi

Re: Switch labels (null again), some tweaking

[Brian Goetz]

Indeed.  It's not clear how much work it is worth doing to discover that 
the reason _why_ we're in the remainder is that we had a pattern:


    case Foo(Bar(Baz(Mumble(Soup s:

and someone passed us a Foo(Bar(Baz(Mumble(pizza.

We could statically emit a description of the remainder, but it would 
get large and esoteric quickly if pattern nesting got "deep" or "wide".  
Seems mostly like an ugly secret the compiler should keep to itself.



On 4/29/2021 10:48 AM, Maurizio Cimadamore wrote:



On 29/04/2021 15:46, Brian Goetz wrote:
I don't think we want the compiler generating tons of code just so 
each remainder can get a different exception; more likely, the 
compiler will want to generate some sort of "default: 
throwSomethingSimple" clause. 


Yeah - that's my understanding, as far as code generation goes.

I guess an interesting question, for when we generate better error 
messages to show remainder, would be how to "spell" (e.g. in the 
diagnostic) those remainders associated with not-yet known types.


But that's a question for another day.

Maurizio

Re: Switch labels (null again), some tweaking

[Brian Goetz]

Without diving into the translation details prematurely, I just want to 
note that we *do* want the compiler to "totalize" things for us, 
because, DA.  Suppose we have A permits B, C:


    int x ;
    switch (a) {
    case B(int foo): x = foo; break;
    case C(int bar): x = bar; break;
    }
    // HERE

There is some remainder -- null, D -- but we don't want that remainder 
to leak past the switch; when we get to HERE, we'd like x to be DA, and 
a to have matched one of the patterns.  So the compiler has to insert 
_something_ to handle the remaining cases, even if it is only:


    default: throw new TotalityException("blah blah");

But, the details of code generation are not what M is asking about now 
-- he's asking "if I were the user, could I write a truly covering 
switch?"  And the answer is yes, but the shape of the remainder is 
"spiny" and can get complicated quickly.



Not necessarily.

First, let's acknowledge that you are moving the discussion from the basic 
semantics to talk about the translation strategy which touch more the binary 
compatibility,
aka, what is the semantics when the view of the world at compile time and at 
runtime are disagreeing.

There are at least two reasons to let javac emits such cases,
first like with null as remainder, you have to add a lot of cases once you have 
sub-patterns, so it will bloat the bytecode,
then if we insert such cases, it means that we also have a code that throw a 
specific exception bolt into the bytecode which means that we can not change 
the binary compatibility story later.

The jobs to implement the binary compatibility semantics is the job of the 
runtime not the compiler, like with lambdas, where the LambdaMetaFactory does 
some runtime checks before generating + linking the lambda proxy,
I expect a SwitchMetafactory to do the same job. This is more flexible and 
allows the runtime to be updated when the VM change by example, the 
lambdaMetafactory code was changed with the introduction of hidden classes.

Now, the big question is what binary compatibility semantics we want ?

We can by example throw a subclass of LinkageError upfront during the linking 
when we detect that the sealed type as more subclasses that the one accessible 
at compile time, but it means that adding a new subclass to a sealed type is 
not a binary compatible change anymore. We can delay the detection the an 
incompatible class until we see one at runtime, so adding a new subclass is a 
compatible change but calling a switch with an instance of such subclass is not.

There is also the question about the order of the cases, should the order of the 
cases be validated at runtime or not, by example, if we have B < A at compile time 
but A < B at runtime with a switch that like case B first and case A second.


Maurizio

Rémi

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

On 29/04/2021 15:46, Brian Goetz wrote:
I don't think we want the compiler generating tons of code just so 
each remainder can get a different exception; more likely, the 
compiler will want to generate some sort of "default: 
throwSomethingSimple" clause. 


Yeah - that's my understanding, as far as code generation goes.

I guess an interesting question, for when we generate better error 
messages to show remainder, would be how to "spell" (e.g. in the 
diagnostic) those remainders associated with not-yet known types.


But that's a question for another day.

Maurizio

Re: Switch labels (null again), some tweaking

[Brian Goetz]

Whenever you have a deconstruction pattern, there's always a remainder 
null. (Point(var x, var y) NPEs on null.)


Whenever you cover a sealed type with alternatives (but no total 
pattern), there's always remainder null and "novel".


Whenever you lift over a nestable pattern (like D(T), or String[] { P 
}), you have to wrap the remainder with the nestable thing.


So yes, Container(Pizza) is also remainder.

Based on historical precedent, its tempting to specify NPE for null 
remainder and ICCE for novel remainder.  (I can also imagine cases where 
the logical exception type is CCE.)  But that doesn't scale up very 
well; what do we throw for DoubleLunchPack(null, pizza)?  It has both 
null- and novel-derived remainders.  I don't think we want the compiler 
generating tons of code just so each remainder can get a different 
exception; more likely, the compiler will want to generate some sort of 
"default: throwSomethingSimple" clause.



On 4/29/2021 5:43 AM, Maurizio Cimadamore wrote:




If I read the rules correctly, Box(Soup) + Bag(Soup) "cover" 
Container, with the exception of the { null, Box(null), 
Bag(null) }. So the above will throw when `lunch` is null, and will 
also throw with Box(null) or Bag(null). Correct?




Correct (under the "we make switches total" plan.)


I realized there's also another remainder Box/Bag(*) - e.g. 
Box/Bag(Pizza), where Pizza is a new type that shows up in the sealed 
hierarchy.


To cover that (not that it's required at compile-time, just to imagine 
what javac would emit), we need probably one of these:


case Box b:

or

case Container c

Right?

Maurizio

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

On 29/04/2021 13:17, fo...@univ-mlv.fr wrote:

Not necessarily.

First, let's acknowledge that you are moving the discussion from the basic 
semantics to talk about the translation strategy which touch more the binary 
compatibility,
aka, what is the semantics when the view of the world at compile time and at 
runtime are disagreeing.


I wasn't necessarily yet talking about translation strategy - as much I 
was trying to understand what a user could do to "bullet proof" its 
switches. It seems to me that there's a way to name almost all the 
components of a remainder, except for the "unknown" ones (which come 
from sealed hiearchies).


I'm not (yet) concerned with bytecode considerations :-)

Maurizio

Re: Switch labels (null again), some tweaking

[forax]

- Mail original -
> De: "Maurizio Cimadamore" 
> À: "Brian Goetz" , "Remi Forax" 
> Cc: "amber-spec-experts" 
> Envoyé: Jeudi 29 Avril 2021 11:43:54
> Objet: Re: Switch labels (null again), some tweaking

>>>
>>> If I read the rules correctly, Box(Soup) + Bag(Soup) "cover"
>>> Container, with the exception of the { null, Box(null),
>>> Bag(null) }. So the above will throw when `lunch` is null, and will
>>> also throw with Box(null) or Bag(null). Correct?
>>>
>>
>> Correct (under the "we make switches total" plan.)
> 
> I realized there's also another remainder Box/Bag(*) - e.g.
> Box/Bag(Pizza), where Pizza is a new type that shows up in the sealed
> hierarchy.
> 
> To cover that (not that it's required at compile-time, just to imagine
> what javac would emit), we need probably one of these:
> 
> case Box b:
> 
> or
> 
> case Container c
> 
> Right?


Not necessarily.

First, let's acknowledge that you are moving the discussion from the basic 
semantics to talk about the translation strategy which touch more the binary 
compatibility,
aka, what is the semantics when the view of the world at compile time and at 
runtime are disagreeing.

There are at least two reasons to let javac emits such cases,
first like with null as remainder, you have to add a lot of cases once you have 
sub-patterns, so it will bloat the bytecode,
then if we insert such cases, it means that we also have a code that throw a 
specific exception bolt into the bytecode which means that we can not change 
the binary compatibility story later.

The jobs to implement the binary compatibility semantics is the job of the 
runtime not the compiler, like with lambdas, where the LambdaMetaFactory does 
some runtime checks before generating + linking the lambda proxy,
I expect a SwitchMetafactory to do the same job. This is more flexible and 
allows the runtime to be updated when the VM change by example, the 
lambdaMetafactory code was changed with the introduction of hidden classes.

Now, the big question is what binary compatibility semantics we want ?

We can by example throw a subclass of LinkageError upfront during the linking 
when we detect that the sealed type as more subclasses that the one accessible 
at compile time, but it means that adding a new subclass to a sealed type is 
not a binary compatible change anymore. We can delay the detection the an 
incompatible class until we see one at runtime, so adding a new subclass is a 
compatible change but calling a switch with an instance of such subclass is not.

There is also the question about the order of the cases, should the order of 
the cases be validated at runtime or not, by example, if we have B < A at 
compile time but A < B at runtime with a switch that like case B first and case 
A second.

> 
> Maurizio

Rémi

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

If I read the rules correctly, Box(Soup) + Bag(Soup) "cover" 
Container, with the exception of the { null, Box(null), 
Bag(null) }. So the above will throw when `lunch` is null, and will 
also throw with Box(null) or Bag(null). Correct?




Correct (under the "we make switches total" plan.)


I realized there's also another remainder Box/Bag(*) - e.g. 
Box/Bag(Pizza), where Pizza is a new type that shows up in the sealed 
hierarchy.


To cover that (not that it's required at compile-time, just to imagine 
what javac would emit), we need probably one of these:


case Box b:

or

case Container c

Right?

Maurizio

Re: Switch labels (null again), some tweaking

[Guy Steele]

I like “covers” better than the best phrase I came up with, which was 
“ostensibly exhaustive”.  :-)

This looks like a good recap.

—Guy

> On Apr 28, 2021, at 4:11 PM, Brian Goetz  wrote:
> 
> Armed with this observation, here's a restack of the terminology and rules, 
> but with no semantic differences from the current story, just new names.  
> 
> The basic idea is: 
>  total on T with no remainder -> total on T
>  total on T with remainder R -> covers T, excepting/modulo R
> 
> 
> Concepts:
>  - A pattern P can be _total_ on a type T.  Total patterns match every 
> element of the value set of T, including null.  
>  - A set of patterns P* can _cover_ a type T, excepting/modulo R*.  This 
> means that for every element in the value set of T that is not matched by 
> some pattern in R*, it is matched by some pattern in P*.  
>  - If P is total on T, { P } covers T (with no exceptions.)
> 
> Base cases:
>  - (type patterns) The type pattern `T t` is total on all U <: T
>  - (var patterns) The var pattern `var x` is total on all T
>  - (default) The label `default` corresponds to a pattern that covers all 
> types, modulo null.  
>  - (sealing) For an abstract sealed type S permitting T0..Tn, the set of 
> patterns { T0, T1, ... Tn } covers S, modulo null and novel subtypes of S.  
> 
> Induction cases:
>  - (lifting) For a deconstruction pattern D(T), { D(Q) : Q in Q* } covers D 
> (modulo D(R*) and null) iff Q* covers T modulo R.  
> 
> 
> Construct restrictions: 
>  - The pattern on the RHS of instanceof may not be total on the type of the 
> LHS.  
>  - In a (non-legacy) switch on x : T, the set of patterns in the case labels 
> must cover T, excepting some remainder.  It throws on the remainder.
>  - In a pattern assignment `P = e`, where `e : T`, P must be cover T.  It 
> throws on the remainder.
> 
> 
> This is just a restack of the terms, but I think it eliminates the most 
> problematic part, which is 'total with remainder'.  Now, total means total.  
> Total with remainder becomes "covers, excepting".  
> 
> 
> 
> 
> On 4/28/2021 2:13 PM, Brian Goetz wrote:
>> I think you're right that the terminology is currently biased for 
>> mathematicians, which is a necessary initial phase to prove that the 
>> language is   right, but needs to get to the part where the 
>> terminology makes sense to Joe Java.  
>> 
>> The notion of "total with remainder" is indeed confusing, and we need to 
>> find a better way to say it, but we come by it honestly.  Because the 
>> "remainder" corresponds to cases where no reasonable Java developer would 
>> want to be forced to write them out, such as "novel enum value".  
>> 
>> I think we can make things slightly (but not enough) better by using "total" 
>> for single patterns only, and using "exhaustive" for sets of patterns, since 
>> that's what drives switch exhaustiveness.  
>> 
>> But that's only a start.
>> 
>> On 4/28/2021 2:09 PM, Maurizio Cimadamore wrote:
>>> I think I got the two main fallacies which led me down the wrong path:
>>> 
>>> 1. there is a distinction between patterns that are total on T, and 
>>> patterns that are total on T, but with a "remainder"
>>> 
>>> 2. there is a distinction between a pattern being total on T, and a set of 
>>> patterns being total (or exhaustive) on T
>>> 
>>> This sent me completely haywire, because I was trying to reason in terms of 
>>> what a plain pattern instanceof would consider "total", and then translate 
>>> the results to nested patterns in switch - and that didn't work, because 
>>> two different sets of rules apply there.
>>> 
>>> Maurizio
>>> 
>>> On 28/04/2021 18:27, Brian Goetz wrote:
 I think part of the problem is that we're using the word "total" in 
 different ways.  
 
 A pattern P may be total on type T with remainder R.  For example, the 
 pattern `Soup s` is total on `Soup` with no remainder.
 
 A _set_ of patterns may be total on T with remainder R as well.  (The only 
 way a set of patterns is total is either (a) one of the patterns in the 
 set is already total on T, OR (b) sealing comes into play.)  Maybe this 
 should be called "exhaustive" to separate from pattern totality.
 
 Switch exhaustiveness derives from set-totality.  
 
 Instanceof prohibits patterns that are total without remainder, for two 
 reasons: (1) its silly to ask a question which constant-folds to `true`, 
 and (b) the disagreement between traditional `instanceof Object` and 
 `instanceof ` at null would likely be a source of bugs.  
 (This was the cost of reusing instanceof rather than creating a new 
 "matches" operator.)  
 
> Foo x = ... 
> if (x instanceof Bar) 
> 
> The instanceof will not be considered total, and therefore be accepted by 
> the compiler (sorry to repeat the same question - I want to make sure I 
> understand how totality works with sealed hierarchies).
> 
 
 If the RHS of an 

Re: Switch labels (null again), some tweaking

[Brian Goetz]

On 4/28/2021 5:34 PM, Maurizio Cimadamore wrote:


Thanks for this.

It is especially helpful to see all the rules in a single place.

So, armed with these rules - back to the first example I brought up:

switch (lunch) {
    case Box(Soup s) {
 if (s == null) {
  System.err.println("Box of null");
 } else {
  System.err.println("Box of soup");
 }
    }

    case Bag(Soup s): {
             if (s == null) {
  System.err.println("Bag of null");
 } else {
  System.err.println("Bag of soup");
 }

    }
}

If I read the rules correctly, Box(Soup) + Bag(Soup) "cover" 
Container, with the exception of the { null, Box(null), 
Bag(null) }. So the above will throw when `lunch` is null, and will 
also throw with Box(null) or Bag(null). Correct?




Correct (under the "we make switches total" plan.)

So the right way to write that would be to add a couple of { case 
Box(null), case Bag(null) } - these will reduce the remainder of the 
switch blanket to just { null } - which means the switch will just 
throw on a null input value, as usual.




Correct.  Any of the following would work to capture the remainder 
explicitly (not all of these are valid syntax, though):


    case null, Box(null), Bag(null):   // explicit remainder

    case null, Box, Bag: // basically the same

    case null, default:   // default misses null, so we add it in

    case null, Container(null): // another way to say the same thing

    case Container c:   // total pattern, catches everything

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

Thanks for this.

It is especially helpful to see all the rules in a single place.

So, armed with these rules - back to the first example I brought up:

switch (lunch) {
    case Box(Soup s) {
 if (s == null) {
  System.err.println("Box of null");
 } else {
  System.err.println("Box of soup");
 }
    }

    case Bag(Soup s): {
             if (s == null) {
  System.err.println("Bag of null");
 } else {
  System.err.println("Bag of soup");
 }

    }
}

If I read the rules correctly, Box(Soup) + Bag(Soup) "cover" 
Container, with the exception of the { null, Box(null), Bag(null) 
}. So the above will throw when `lunch` is null, and will also throw 
with Box(null) or Bag(null). Correct?


So the right way to write that would be to add a couple of { case 
Box(null), case Bag(null) } - these will reduce the remainder of the 
switch blanket to just { null } - which means the switch will just throw 
on a null input value, as usual.


Assuming I got it correct, I think that if we can get javac to spit out 
all the elements in the remainder (as in the list I wrote above), then 
it should be possible for users to understand what's going wrong, and 
how to fix it.


Maurizio

On 28/04/2021 21:11, Brian Goetz wrote:
Armed with this observation, here's a restack of the terminology and 
rules, but with no semantic differences from the current story, just 
new names.


The basic idea is:
 total on T with no remainder -> total on T
 total on T with remainder R -> covers T, excepting/modulo R


Concepts:
 - A pattern P can be _total_ on a type T.  Total patterns match every 
element of the value set of T, including null.
 - A set of patterns P* can _cover_ a type T, excepting/modulo R*.  
This means that for every element in the value set of T that is not 
matched by some pattern in R*, it is matched by some pattern in P*.

 - If P is total on T, { P } covers T (with no exceptions.)

Base cases:
 - (type patterns) The type pattern `T t` is total on all U <: T
 - (var patterns) The var pattern `var x` is total on all T
 - (default) The label `default` corresponds to a pattern that covers 
all types, modulo null.
 - (sealing) For an abstract sealed type S permitting T0..Tn, the set 
of patterns { T0, T1, ... Tn } covers S, modulo null and novel 
subtypes of S.


Induction cases:
 - (lifting) For a deconstruction pattern D(T), { D(Q) : Q in Q* } 
covers D (modulo D(R*) and null) iff Q* covers T modulo R.



Construct restrictions:
 - The pattern on the RHS of instanceof may not be total on the type 
of the LHS.
 - In a (non-legacy) switch on x : T, the set of patterns in the case 
labels must cover T, excepting some remainder.  It throws on the 
remainder.
 - In a pattern assignment `P = e`, where `e : T`, P must be cover T. 
It throws on the remainder.



This is just a restack of the terms, but I think it eliminates the 
most problematic part, which is 'total with remainder'.  Now, total 
means total.  Total with remainder becomes "covers, excepting".





On 4/28/2021 2:13 PM, Brian Goetz wrote:
I think you're right that the terminology is currently biased for 
mathematicians, which is a necessary initial phase to prove that the 
language is right, but needs to get to the part where the terminology 
makes sense to Joe Java.


The notion of "total with remainder" is indeed confusing, and we need 
to find a better way to say it, but we come by it honestly.  Because 
the "remainder" corresponds to cases where no reasonable Java 
developer would want to be forced to write them out, such as "novel 
enum value".


I think we can make things slightly (but not enough) better by using 
"total" for single patterns only, and using "exhaustive" for sets of 
patterns, since that's what drives switch exhaustiveness.


But that's only a start.

On 4/28/2021 2:09 PM, Maurizio Cimadamore wrote:


I think I got the two main fallacies which led me down the wrong path:

1. there is a distinction between patterns that are total on T, and 
patterns that are total on T, but with a "remainder"


2. there is a distinction between a pattern being total on T, and a 
set of patterns being total (or exhaustive) on T


This sent me completely haywire, because I was trying to reason in 
terms of what a plain pattern instanceof would consider "total", and 
then translate the results to nested patterns in switch - and that 
didn't work, because two different sets of rules apply there.


Maurizio

On 28/04/2021 18:27, Brian Goetz wrote:
I think part of the problem is that we're using the word "total" in 
different ways.


A pattern P may be total on type T with remainder R. For example, 
the pattern `Soup s` is total on `Soup` with no remainder.


A _set_ of patterns may be total on T with remainder R as well.  
(The only way a set of patterns is total is either (a) one of the 
patterns in the set is already total on

Re: Switch labels (null again), some tweaking

[Brian Goetz]

Armed with this observation, here's a restack of the terminology and 
rules, but with no semantic differences from the current story, just new 
names.


The basic idea is:
 total on T with no remainder -> total on T
 total on T with remainder R -> covers T, excepting/modulo R


Concepts:
 - A pattern P can be _total_ on a type T.  Total patterns match every 
element of the value set of T, including null.
 - A set of patterns P* can _cover_ a type T, excepting/modulo R*.  
This means that for every element in the value set of T that is not 
matched by some pattern in R*, it is matched by some pattern in P*.

 - If P is total on T, { P } covers T (with no exceptions.)

Base cases:
 - (type patterns) The type pattern `T t` is total on all U <: T
 - (var patterns) The var pattern `var x` is total on all T
 - (default) The label `default` corresponds to a pattern that covers 
all types, modulo null.
 - (sealing) For an abstract sealed type S permitting T0..Tn, the set 
of patterns { T0, T1, ... Tn } covers S, modulo null and novel subtypes 
of S.


Induction cases:
 - (lifting) For a deconstruction pattern D(T), { D(Q) : Q in Q* } 
covers D (modulo D(R*) and null) iff Q* covers T modulo R.



Construct restrictions:
 - The pattern on the RHS of instanceof may not be total on the type of 
the LHS.
 - In a (non-legacy) switch on x : T, the set of patterns in the case 
labels must cover T, excepting some remainder.  It throws on the remainder.
 - In a pattern assignment `P = e`, where `e : T`, P must be cover T. 
It throws on the remainder.



This is just a restack of the terms, but I think it eliminates the most 
problematic part, which is 'total with remainder'.  Now, total means 
total.  Total with remainder becomes "covers, excepting".





On 4/28/2021 2:13 PM, Brian Goetz wrote:
I think you're right that the terminology is currently biased for 
mathematicians, which is a necessary initial phase to prove that the 
language is right, but needs to get to the part where the terminology 
makes sense to Joe Java.


The notion of "total with remainder" is indeed confusing, and we need 
to find a better way to say it, but we come by it honestly.  Because 
the "remainder" corresponds to cases where no reasonable Java 
developer would want to be forced to write them out, such as "novel 
enum value".


I think we can make things slightly (but not enough) better by using 
"total" for single patterns only, and using "exhaustive" for sets of 
patterns, since that's what drives switch exhaustiveness.


But that's only a start.

On 4/28/2021 2:09 PM, Maurizio Cimadamore wrote:


I think I got the two main fallacies which led me down the wrong path:

1. there is a distinction between patterns that are total on T, and 
patterns that are total on T, but with a "remainder"


2. there is a distinction between a pattern being total on T, and a 
set of patterns being total (or exhaustive) on T


This sent me completely haywire, because I was trying to reason in 
terms of what a plain pattern instanceof would consider "total", and 
then translate the results to nested patterns in switch - and that 
didn't work, because two different sets of rules apply there.


Maurizio

On 28/04/2021 18:27, Brian Goetz wrote:
I think part of the problem is that we're using the word "total" in 
different ways.


A pattern P may be total on type T with remainder R.  For example, 
the pattern `Soup s` is total on `Soup` with no remainder.


A _set_ of patterns may be total on T with remainder R as well.  
(The only way a set of patterns is total is either (a) one of the 
patterns in the set is already total on T, OR (b) sealing comes into 
play.)  Maybe this should be called "exhaustive" to separate from 
pattern totality.


Switch exhaustiveness derives from set-totality.

Instanceof prohibits patterns that are total without remainder, for 
two reasons: (1) its silly to ask a question which constant-folds to 
`true`, and (b) the disagreement between traditional `instanceof 
Object` and `instanceof ` at null would likely be a 
source of bugs.  (This was the cost of reusing instanceof rather 
than creating a new "matches" operator.)



Foo x = ...
if (x instanceof Bar)

The instanceof will not be considered total, and therefore be 
accepted by the compiler (sorry to repeat the same question - I 
want to make sure I understand how totality works with sealed 
hierarchies).




If the RHS of an `instanceof` is a type (not a type pattern), then 
this has traditional `instanceof` behavior.  If Bar <: Foo, then 
this is in effect a null check.


If the RHS is a _pattern_, then the pattern must not be total 
without remainder.  If Bar <: Foo, `Bar b` is total on Foo, so the 
compiler says "dumb question, ask a different one."


If the RHS is a non-total pattern, or a total pattern with 
remainder, then there's a real question being asked.  So in your 
Lunch-permits-Soup example, you could say


    if (lunch instanceof Soup s)

and this matches _on non-null

Re: Switch labels (null again), some tweaking

[Brian Goetz]

I think you're right that the terminology is currently biased for 
mathematicians, which is a necessary initial phase to prove that the 
language is right, but needs to get to the part where the terminology 
makes sense to Joe Java.


The notion of "total with remainder" is indeed confusing, and we need to 
find a better way to say it, but we come by it honestly.  Because the 
"remainder" corresponds to cases where no reasonable Java developer 
would want to be forced to write them out, such as "novel enum value".


I think we can make things slightly (but not enough) better by using 
"total" for single patterns only, and using "exhaustive" for sets of 
patterns, since that's what drives switch exhaustiveness.


But that's only a start.

On 4/28/2021 2:09 PM, Maurizio Cimadamore wrote:


I think I got the two main fallacies which led me down the wrong path:

1. there is a distinction between patterns that are total on T, and 
patterns that are total on T, but with a "remainder"


2. there is a distinction between a pattern being total on T, and a 
set of patterns being total (or exhaustive) on T


This sent me completely haywire, because I was trying to reason in 
terms of what a plain pattern instanceof would consider "total", and 
then translate the results to nested patterns in switch - and that 
didn't work, because two different sets of rules apply there.


Maurizio

On 28/04/2021 18:27, Brian Goetz wrote:
I think part of the problem is that we're using the word "total" in 
different ways.


A pattern P may be total on type T with remainder R.  For example, 
the pattern `Soup s` is total on `Soup` with no remainder.


A _set_ of patterns may be total on T with remainder R as well.  (The 
only way a set of patterns is total is either (a) one of the patterns 
in the set is already total on T, OR (b) sealing comes into play.)  
Maybe this should be called "exhaustive" to separate from pattern 
totality.


Switch exhaustiveness derives from set-totality.

Instanceof prohibits patterns that are total without remainder, for 
two reasons: (1) its silly to ask a question which constant-folds to 
`true`, and (b) the disagreement between traditional `instanceof 
Object` and `instanceof ` at null would likely be a 
source of bugs.  (This was the cost of reusing instanceof rather than 
creating a new "matches" operator.)



Foo x = ...
if (x instanceof Bar)

The instanceof will not be considered total, and therefore be 
accepted by the compiler (sorry to repeat the same question - I want 
to make sure I understand how totality works with sealed hierarchies).




If the RHS of an `instanceof` is a type (not a type pattern), then 
this has traditional `instanceof` behavior.  If Bar <: Foo, then this 
is in effect a null check.


If the RHS is a _pattern_, then the pattern must not be total without 
remainder.  If Bar <: Foo, `Bar b` is total on Foo, so the compiler 
says "dumb question, ask a different one."


If the RHS is a non-total pattern, or a total pattern with remainder, 
then there's a real question being asked.  So in your 
Lunch-permits-Soup example, you could say


    if (lunch instanceof Soup s)

and this matches _on non-null lunch_.  Just like the switch.  The 
only difference is switch will throw on unmatched nulls, whereas 
instanceof says "no, not an instance", but that's got nothing to do 
with patterns, it's about conditional constructs.


If that's the case, I find that a bit odd - because enums kind of 
have the same issue (but we have opted to trust that a switch on an 
enum is total if all the constants known at compile time are 
covered) - and, to my eyes, if you squint, a sealed hierarchy is 
like an enum for types (e.g. sum type).




OK, let's talk about enums.  Suppose I have:

    enum Lunch { Soup }

and I do

    switch (lunch) {
    case Soup -> ...
    }

What happens on null?  It throws, and it always has.  The behavior 
for the sealed analogue is the same; the `Soup s` pattern matches the 
non-null lunches, and if null is left unhandled elsewhere in the 
switch, the switch throws.  No asymmetry.



Anyway, backing up - this below:

```

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();
    }
```

is good code, which says what it means. I think the challenge will 
be to present error messages (e.g. if the user forgot to add case 
Box(null)) in a way that makes it clear to the user as to what's 
missing; and maybe that will be enough.




The challenge here is that we don't want to force the user to handle 
the "silly" cases, such as:


    Boolean bool = ...
    switch (bool) {
    case true -> ...
    case false -> ...
    case null -> ...  // who would be happy about having to write 
this case?

    }

and the similarly lifted:

    

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

I think I got the two main fallacies which led me down the wrong path:

1. there is a distinction between patterns that are total on T, and 
patterns that are total on T, but with a "remainder"


2. there is a distinction between a pattern being total on T, and a set 
of patterns being total (or exhaustive) on T


This sent me completely haywire, because I was trying to reason in terms 
of what a plain pattern instanceof would consider "total", and then 
translate the results to nested patterns in switch - and that didn't 
work, because two different sets of rules apply there.


Maurizio

On 28/04/2021 18:27, Brian Goetz wrote:
I think part of the problem is that we're using the word "total" in 
different ways.


A pattern P may be total on type T with remainder R.  For example, the 
pattern `Soup s` is total on `Soup` with no remainder.


A _set_ of patterns may be total on T with remainder R as well.  (The 
only way a set of patterns is total is either (a) one of the patterns 
in the set is already total on T, OR (b) sealing comes into play.)  
Maybe this should be called "exhaustive" to separate from pattern 
totality.


Switch exhaustiveness derives from set-totality.

Instanceof prohibits patterns that are total without remainder, for 
two reasons: (1) its silly to ask a question which constant-folds to 
`true`, and (b) the disagreement between traditional `instanceof 
Object` and `instanceof ` at null would likely be a 
source of bugs.  (This was the cost of reusing instanceof rather than 
creating a new "matches" operator.)



Foo x = ...
if (x instanceof Bar)

The instanceof will not be considered total, and therefore be 
accepted by the compiler (sorry to repeat the same question - I want 
to make sure I understand how totality works with sealed hierarchies).




If the RHS of an `instanceof` is a type (not a type pattern), then 
this has traditional `instanceof` behavior.  If Bar <: Foo, then this 
is in effect a null check.


If the RHS is a _pattern_, then the pattern must not be total without 
remainder.  If Bar <: Foo, `Bar b` is total on Foo, so the compiler 
says "dumb question, ask a different one."


If the RHS is a non-total pattern, or a total pattern with remainder, 
then there's a real question being asked.  So in your 
Lunch-permits-Soup example, you could say


    if (lunch instanceof Soup s)

and this matches _on non-null lunch_.  Just like the switch. The only 
difference is switch will throw on unmatched nulls, whereas instanceof 
says "no, not an instance", but that's got nothing to do with 
patterns, it's about conditional constructs.


If that's the case, I find that a bit odd - because enums kind of 
have the same issue (but we have opted to trust that a switch on an 
enum is total if all the constants known at compile time are covered) 
- and, to my eyes, if you squint, a sealed hierarchy is like an enum 
for types (e.g. sum type).




OK, let's talk about enums.  Suppose I have:

    enum Lunch { Soup }

and I do

    switch (lunch) {
    case Soup -> ...
    }

What happens on null?  It throws, and it always has.  The behavior for 
the sealed analogue is the same; the `Soup s` pattern matches the 
non-null lunches, and if null is left unhandled elsewhere in the 
switch, the switch throws.  No asymmetry.



Anyway, backing up - this below:

```

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();
    }
```

is good code, which says what it means. I think the challenge will be 
to present error messages (e.g. if the user forgot to add case 
Box(null)) in a way that makes it clear to the user as to what's 
missing; and maybe that will be enough.




The challenge here is that we don't want to force the user to handle 
the "silly" cases, such as:


    Boolean bool = ...
    switch (bool) {
    case true -> ...
    case false -> ...
    case null -> ...  // who would be happy about having to write 
this case?

    }

and the similarly lifted:

    Box box = ...
    switch (box) {
    case Box(true) -> ...
    case Box(false) -> ...
    case Box(null) -> ...  // who would be happy about having to 
write this case?

    case Box(novel) -> ... // or this case?
    case null ->   // or this case?
    }

So we define the "remainder" as the values that "fall into the cracks 
between the patterns."  Users can write patterns for these, and 
they'll match, but if not, the compiler inserts code to catch these 
and throw something.


The benefit is twofold: not only does the user not have to write the 
stupid cases (imagine if Box had ten slots, would we want to write the 
2^10 partial null cases?), but because we throw on the remainder, DA 
can treat the switch as covering all boxes, and be assured there are 
no l

Re: Switch labels (null again), some tweaking

[Brian Goetz]

The benefit is twofold: not only does the user not have to write the 
stupid cases (imagine if Box had ten slots, would we want to write the 
2^10 partial null cases?), but because we throw on the remainder, DA 
can treat the switch as covering all boxes, and be assured there are 
no leaks.


More on this last point.  We don't yet have pattern assignment, but 
totality and remainder are key to it.  Suppose we have


    Box bs = ...

and we want to destructure:

    Box(String s) = bs;
    // s had better be DA here

The pattern on the LHS must be total, but can have remainder; the 
statement is allowed to throw on the remainder, because the remainder 
is, by definition, the "silly" matches.  Here, the only remainder is 
null; you can't destructure a null, so if you asked to destructure a 
Box, you probably were assuming that it was a real box.  So this 
assignment NPEs on null (not unlike the corresponding switch).

Re: Switch labels (null again), some tweaking

[Brian Goetz]

I think part of the problem is that we're using the word "total" in 
different ways.


A pattern P may be total on type T with remainder R.  For example, the 
pattern `Soup s` is total on `Soup` with no remainder.


A _set_ of patterns may be total on T with remainder R as well. (The 
only way a set of patterns is total is either (a) one of the patterns in 
the set is already total on T, OR (b) sealing comes into play.)  Maybe 
this should be called "exhaustive" to separate from pattern totality.


Switch exhaustiveness derives from set-totality.

Instanceof prohibits patterns that are total without remainder, for two 
reasons: (1) its silly to ask a question which constant-folds to `true`, 
and (b) the disagreement between traditional `instanceof Object` and 
`instanceof ` at null would likely be a source of bugs.  
(This was the cost of reusing instanceof rather than creating a new 
"matches" operator.)



Foo x = ...
if (x instanceof Bar)

The instanceof will not be considered total, and therefore be accepted 
by the compiler (sorry to repeat the same question - I want to make 
sure I understand how totality works with sealed hierarchies).




If the RHS of an `instanceof` is a type (not a type pattern), then this 
has traditional `instanceof` behavior.  If Bar <: Foo, then this is in 
effect a null check.


If the RHS is a _pattern_, then the pattern must not be total without 
remainder.  If Bar <: Foo, `Bar b` is total on Foo, so the compiler says 
"dumb question, ask a different one."


If the RHS is a non-total pattern, or a total pattern with remainder, 
then there's a real question being asked.  So in your Lunch-permits-Soup 
example, you could say


    if (lunch instanceof Soup s)

and this matches _on non-null lunch_.  Just like the switch. The only 
difference is switch will throw on unmatched nulls, whereas instanceof 
says "no, not an instance", but that's got nothing to do with patterns, 
it's about conditional constructs.


If that's the case, I find that a bit odd - because enums kind of have 
the same issue (but we have opted to trust that a switch on an enum is 
total if all the constants known at compile time are covered) - and, 
to my eyes, if you squint, a sealed hierarchy is like an enum for 
types (e.g. sum type).




OK, let's talk about enums. Suppose I have:

    enum Lunch { Soup }

and I do

    switch (lunch) {
    case Soup -> ...
    }

What happens on null?  It throws, and it always has.  The behavior for 
the sealed analogue is the same; the `Soup s` pattern matches the 
non-null lunches, and if null is left unhandled elsewhere in the switch, 
the switch throws.  No asymmetry.



Anyway, backing up - this below:

```

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();
    }
```

is good code, which says what it means. I think the challenge will be 
to present error messages (e.g. if the user forgot to add case 
Box(null)) in a way that makes it clear to the user as to what's 
missing; and maybe that will be enough.




The challenge here is that we don't want to force the user to handle the 
"silly" cases, such as:


    Boolean bool = ...
    switch (bool) {
    case true -> ...
    case false -> ...
    case null -> ...  // who would be happy about having to write 
this case?

    }

and the similarly lifted:

    Box box = ...
    switch (box) {
    case Box(true) -> ...
    case Box(false) -> ...
    case Box(null) -> ...  // who would be happy about having to 
write this case?

    case Box(novel) -> ... // or this case?
    case null ->   // or this case?
    }

So we define the "remainder" as the values that "fall into the cracks 
between the patterns."  Users can write patterns for these, and they'll 
match, but if not, the compiler inserts code to catch these and throw 
something.


The benefit is twofold: not only does the user not have to write the 
stupid cases (imagine if Box had ten slots, would we want to write the 
2^10 partial null cases?), but because we throw on the remainder, DA can 
treat the switch as covering all boxes, and be assured there are no leaks.

Re: Switch labels (null again), some tweaking

[forax]

> De: "Maurizio Cimadamore" 
> À: "Remi Forax" 
> Cc: "Brian Goetz" , "amber-spec-experts"
> 
> Envoyé: Mercredi 28 Avril 2021 19:09:07
> Objet: Re: Switch labels (null again), some tweaking

> On 28/04/2021 18:03, [ mailto:fo...@univ-mlv.fr | fo...@univ-mlv.fr ] wrote:

>> There is no notion of totality for instanceof.

> This is not what I understood when reading Brian message:

>> We made a decision to lump pattern matching in with `instanceof` because it
>> seemed silly to have two almost identical but subtly different constructs for
>> "dynamic type test" and "pattern match" (given that you can do dynamic type
>> tests with patterns.) We knew that this would have some uncomfortable
>> consequences, and what we have tentatively decided to do is outlaw total
>> patterns in instanceof, so that users are not confronted with the subtle
>> difference between `x instanceof Object` and `x instanceof Object o`. This 
>> may
>> not be a totally satisfying answer, and we left some room to adjust this, but
>> its where we are.
> instanceof featuring a pattern that is total w.r.t. the type of the instanceof
> expression is outlawed. Which is why I was bringing that up.
Let me re-phrase it, there is no need for a notion of totality on instanceof. 
(at least at the first level, we need it for sub-patterns) 

> Maurizio

Rémi 

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

On 28/04/2021 18:03, fo...@univ-mlv.fr wrote:

There is no notion of totality for instanceof.


This is not what I understood when reading Brian message:

We made a decision to lump pattern matching in with `instanceof` 
because it seemed silly to have two almost identical but subtly 
different constructs for "dynamic type test" and "pattern match" 
(given that you can do dynamic type tests with patterns.)  We knew 
that this would have some uncomfortable consequences, and what we have 
tentatively decided to do is outlaw total patterns in instanceof, so 
that users are not confronted with the subtle difference between `x 
instanceof Object` and `x instanceof Object o`.  This may not be a 
totally satisfying answer, and we left some room to adjust this, but 
its where we are.


instanceof featuring a pattern that is total w.r.t. the type of the 
instanceof expression is outlawed. Which is why I was bringing that up.


Maurizio

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

On 28/04/2021 17:48, Brian Goetz wrote:
The set of patterns { Box(Soup) } is considered total on Box 
_with remainder { null, Box(null), Box(novel) } _.


The pattern Box(Soup) on its own is total on Box (as opposed to 
Box), with remainder { null }; we'll still NPE if the Box 
itself is null.


The intuition here is that Lunch is still a more abstract type than 
Soup, even if the implementation says "only soup here".  We know that 
this assumption could be violated before we get to runtime.


I think I get this - but I guess this implies that, in my previous example:


Foo x = ...
if (x instanceof Bar)

The instanceof will not be considered total, and therefore be accepted 
by the compiler (sorry to repeat the same question - I want to make sure 
I understand how totality works with sealed hierarchies).


If that's the case, I find that a bit odd - because enums kind of have 
the same issue (but we have opted to trust that a switch on an enum is 
total if all the constants known at compile time are covered) - and, to 
my eyes, if you squint, a sealed hierarchy is like an enum for types 
(e.g. sum type).


That said, I think this discussion kind of demonstrates that reasoning 
about totality is not that straightforward; I believe you can see why I 
jumped to the conclusion that Box must have been total on 
Box (if Soup was the only permitted concrete subtype of Lunch) - 
but it turned out I was barking up the wrong tree. This is surely 
caused, in part, by the fact that I'm less immersed in pattern-land 
(e.g. more an interested follower at a distance); but I think it also 
reflects some genuine complexity when it comes to reasoning about totality.


Anyway, backing up - this below:

```

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();
    }
```

is good code, which says what it means. I think the challenge will be to 
present error messages (e.g. if the user forgot to add case Box(null)) 
in a way that makes it clear to the user as to what's missing; and maybe 
that will be enough.


Maurizio



A normalizing force here is we want the same thing at top level and 
nested level.  If i have:


    Lunch lunch = ...
    switch(lunch) {
    case Soup s:
    }

I should expect the same null treatment as I do in the lifted case:

    Box box = ...
    switch (box) {
    case Box(Soup s): ...
    }

Which we get!  In the first case, the _single pattern_ Soup is not 
individually total on Lunch (Lunch is more abstract), but the _set of 
patterns_ { Soup } is total on Lunch with remainder { null, novel 
subtype of Lunch }, due to sealing, so we are able to conclude the 
switch itself is exhaustive (with some remainder rejected.)   When we 
lift, we get totality with remainder of { Box(null), Box(novel) }, 
plus also { null } because of the lifting.






On 4/28/2021 12:33 PM, Maurizio Cimadamore wrote:


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?

Maurizio

Re: Switch labels (null again), some tweaking

[forax]

- Mail original -
> De: "Maurizio Cimadamore" 
> À: "Brian Goetz" , "Remi Forax" 
> Cc: "amber-spec-experts" 
> 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

Re: Switch labels (null again), some tweaking

[Brian Goetz]

The set of patterns { Box(Soup) } is considered total on Box 
_with remainder { null, Box(null), Box(novel) } _.


The pattern Box(Soup) on its own is total on Box (as opposed to 
Box), with remainder { null }; we'll still NPE if the Box itself 
is null.


The intuition here is that Lunch is still a more abstract type than 
Soup, even if the implementation says "only soup here".  We know that 
this assumption could be violated before we get to runtime.


A normalizing force here is we want the same thing at top level and 
nested level.  If i have:


    Lunch lunch = ...
    switch(lunch) {
    case Soup s:
    }

I should expect the same null treatment as I do in the lifted case:

    Box box = ...
    switch (box) {
    case Box(Soup s): ...
    }

Which we get!  In the first case, the _single pattern_ Soup is not 
individually total on Lunch (Lunch is more abstract), but the _set of 
patterns_ { Soup } is total on Lunch with remainder { null, novel 
subtype of Lunch }, due to sealing, so we are able to conclude the 
switch itself is exhaustive (with some remainder rejected.)   When we 
lift, we get totality with remainder of { Box(null), Box(novel) }, plus 
also { null } because of the lifting.






On 4/28/2021 12:33 PM, Maurizio Cimadamore wrote:


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?

Maurizio

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

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?

Maurizio

Re: Switch labels (null again), some tweaking

[Brian Goetz]

Let's say I start with this:


switch (lunch) {
    case Box(Soup s) {
 if (s == null) {
  System.err.println("Box of null");
 } else {
  System.err.println("Box of soup");
 }
    }

    case Bag(Soup s): {
             if (s == null) {
  System.err.println("Bag of null");
 } else {
  System.err.println("Bag of soup");
 }

    }

}



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.



Then Sandwich is added to the hierarchy. The switch no longer 
compiles, I have to make it total. The following, which is, I believe, 
the first thing that will come to mind:


switch (lunch) {
    case Box(Soup s) {  /* same as before */ }
    case Box(Sandwich s) { ... }
    case Bag(Soup s): { /* same as before */ }
    case Bag(Sandwich s) { ... }
}



With the correct version of the first switch, your first idea for fixing 
it to accomodate sandwiches is correct!  The switch is now total on 
Container, the old cases handle the same thing they did, the new 
cases handle the new cases, and the implicit cases (Box(null) etc) 
handle the same thing they did.


But if it is considered exhaustive, then this will compile, but the 
null handling logic will be in the wrong place, and will be 
essentially dead code (which the user might be unaware of). 


No, because it was dead in the first place too.  Box(null) and Bag(null) 
were always treated as remainder.

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

On 28/04/2021 16:54, Brian Goetz wrote:
The think the I find mildly odd is that when Sandwich is added, it 
might not be enough to add another `case`. If there was null-related 
logic inside `case Box(Soup s):` that would have to be moved 
somewhere else. So while in most cases it will be a straightforward 
refactoring, I can see some puzzlers emerging here.


Can you pull on this string a big? 



Let's say I start with this:


switch (lunch) {
    case Box(Soup s) {
 if (s == null) {
  System.err.println("Box of null");
 } else {
  System.err.println("Box of soup");
 }
    }

    case Bag(Soup s): {
             if (s == null) {
  System.err.println("Bag of null");
 } else {
  System.err.println("Bag of soup");
 }

    }

}


Then Sandwich is added to the hierarchy. The switch no longer compiles, 
I have to make it total. The following, which is, I believe, the first 
thing that will come to mind:


switch (lunch) {
    case Box(Soup s) {  /* same as before */ }
    case Box(Sandwich s) { ... }
    case Bag(Soup s): { /* same as before */ }
    case Bag(Sandwich s) { ... }
}


Now, question: is the above switch considered exhaustive? If not 
(because Box(null) is no longer matched), fine, the user will at least 
have some clue of what's happening.


But if it is considered exhaustive, then this will compile, but the null 
handling logic will be in the wrong place, and will be essentially dead 
code (which the user might be unaware of).


Assuming the above is not exhaustive, the user might then think to tweak 
to do this:


switch (lunch) {
    case Box(Soup s) {  /* same as before */ }
    case Box(Sandwich s) { ... }
    case Bag(Soup s): { /* same as before */ }
    case Bag(Sandwich s) { ... }
    default: ...
}

But that's again incorrect. We still have to move the null handling 
logic from `case Box(Soup)` and `case Box(Bar)` - so, the above code 
doesn't really cut it, since the `null` is nested, and not at the 
toplevel. So the better form would be this:


switch (lunch) {
    case Box(Soup s) { System.err.println("Box of soup"); }
    case Box(Sandwich s) { System.err.println("Box of sandwich"); }
    case Box(var x) { System.err.println("Box of null"); }
    case Bag(Soup s): { System.err.println("Bag of soup"); }
    case Bag(Sandwich s) { System.err.println("Bag of sandwich"); }
    case Bag(var x) { System.err.println("Bag of null"); }
}

I believe this is finally (1) total and (2) preserve the semantics of 
the original code. But it took quite a while to get here. And, in this 
new code, it seems like we're essentially using `case Box(var x)` (or 
`case Box(Object o)` it's the same) to really mean `case Box(null)`. 
Which is brittle - because, with this new code, if a new subtype is 
added (Pizza), the switch will remain total, no error would occur, but 
the could would behave incorrectly because what used to be a 
"catch-null" case has now turned into more than that.


Maurizio

Re: Switch labels (null again), some tweaking

[Brian Goetz]

I guess the case I'm referring to is:

switch (lunch) {
    case Box(Soup s):
    case Bag(Soup s):
}

Where Soup is the only know subtype of Lunch. This code is exhaustive, 
but is Sandwich is added, it is no longer so.


Given Lunch is sealed to only permit Soup, and Container = Box|Bag, then 
this switch is exhaustive on COntainer.


Later, when Lunch is extended to permit Sandwich, this switch becomes 
not exhaustive on Container, and you get a compile error, as you 
would want.  Now you can totalize either by handling the 
sandwich-related cases, OR by adding Box(Lunch)/Box(var) cases, OR by 
adding Container(Soup) cases, OR by adding Container(Lunch) case, OR by 
adding a default/var case.


That said, if an error is issued whenever a switch statement is not 
exhaustive, that would alleviate my concerns - I think the error would 
cover this case also.


Yes.  Totality is compositional.  We can treat `Box(Soup)` as Box(var 
alpha) & alpha matches Soup.  Then the switch is a big disjunction of 
conjunctions, and we can rearrange with De Morgan's laws and related 
boolean algebra tricks.  So


   Box(Soup) OR Box(Sandwich)
   == (Box(var alpha) AND alpha matches Soup) OR (Box(var alpha) AND 
alpha matches Sandwich)

   == Box(var alpha) AND (alpha matches Soup OR alpha matches Sandwich)
   == Box(var alpha) AND (alpha matches Lunch)
   == Box(Lunch)

The think the I find mildly odd is that when Sandwich is added, it 
might not be enough to add another `case`. If there was null-related 
logic inside `case Box(Soup s):` that would have to be moved somewhere 
else. So while in most cases it will be a straightforward refactoring, 
I can see some puzzlers emerging here.


Can you pull on this string a big?

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

On 28/04/2021 15:31, Brian Goetz wrote:
It depends on how much sealing there is.  Suppose we have sealed types 
Container = Box|Bag and Lunch=Soup|Sandwich.  If we are switching on a 
Container:


    switch (lunch) {
    case Box(Soup s):
    case Box(Sandwich s):
    case Bag(Soup s):
    case Bag(Sandwich s):
    }

This switch is exhaustive because:
 - { Soup, Sandwich } is total on on Lunch (with remainder null)
 - therefore { Box(Soup), Box(Sandwich) } is total on Box (with 
remainder null, Box(null) }
 - similarly { Bag(Soup), Bag(Sandwich) } is total on Bag (with 
remainder null, Bag(null) }

 - { Box, Bag } is total on Container (with remainder null)
 - therefore the cases in our switch are exhaustive on Container


I guess the case I'm referring to is:

switch (lunch) {
    case Box(Soup s):
    case Bag(Soup s):
}

Where Soup is the only know subtype of Lunch. This code is exhaustive, 
but is Sandwich is added, it is no longer so.


That said, if an error is issued whenever a switch statement is not 
exhaustive, that would alleviate my concerns - I think the error would 
cover this case also.


The think the I find mildly odd is that when Sandwich is added, it might 
not be enough to add another `case`. If there was null-related logic 
inside `case Box(Soup s):` that would have to be moved somewhere else. 
So while in most cases it will be a straightforward refactoring, I can 
see some puzzlers emerging here.


Maurizio

Re: Switch labels (null again), some tweaking

[Brian Goetz]

At least, if you want a total type, you can make it explicit using
  case var x
which is always total whatever the type switched upon.

So you have two tools to avoid influence at distance in the totality 
analysis,
- for a switch where you can enumerate all the values enums, sealed 
type (boolean should be in that category too IMO, but we did not 
agree on that), if you list all the possible cases, a total case is 
not required.


Without changes to switch, there is nothing which would break if a 
"new case" is added (to the enum, or to the sealed hierarchy). So, 
listing "all possible cases" relies on the assumption that you know 
what "all cases" are. And right now there's no way to declaratively 
say: this switch (statement) is gonna cover them all. Brian answer 
goes a bit in that direction, which is good, for the outermost layer 
(but the problem still exists somewhat at the nested level).




It depends on how much sealing there is.  Suppose we have sealed types 
Container = Box|Bag and Lunch=Soup|Sandwich.  If we are switching on a 
Container:


    switch (lunch) {
    case Box(Soup s):
    case Box(Sandwich s):
    case Bag(Soup s):
    case Bag(Sandwich s):
    }

This switch is exhaustive because:
 - { Soup, Sandwich } is total on on Lunch (with remainder null)
 - therefore { Box(Soup), Box(Sandwich) } is total on Box (with 
remainder null, Box(null) }
 - similarly { Bag(Soup), Bag(Sandwich) } is total on Bag (with 
remainder null, Bag(null) }

 - { Box, Bag } is total on Container (with remainder null)
 - therefore the cases in our switch are exhaustive on Container

If Lunch were not sealed, the compiler would complain, and we'd need 
extra cases to get totality on Box and on Bag, which is needed to get 
totality on Container:


    switch (lunch) {
    case Box(Soup s):
    case Box(Sandwich s):
    case Box(var s):
    case Bag(Soup s):
    case Bag(Sandwich s):
    case Bag(var s):
    }

So I think its similar at every level.  And you can say `var` or `Lunch` 
or `Object`; they're all total in this context.



- use "var" so the total case is explicit,  "case var x", "case 
Foo(var x)", etc
Sure - this is a good solution. One minor annoying thing is that we 
started from a position where we said "var is just for inference" and 
now we're back in a place where, while  var is still, conceptually at 
least, about inference, developers will also be using it for totality 
(as inference guarantees that you are always 100% covered).


No, you can also say `case Object x` or `case Foo(Object x)` and be 
semantically equivalent.  Var is just type inference here; Remi is 
saying "if you don't want to think about what types are total, say var, 
and you'll be right."  But its just inference for "the minimal type that 
is total."

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

On 28/04/2021 00:44, Remi Forax wrote:





*De: *"Maurizio Cimadamore" 
*À: *"Brian Goetz" , "amber-spec-experts"

*Envoyé: *Mardi 27 Avril 2021 16:23:20
    *Objet: *Re: Switch labels (null again), some tweaking


On 23/04/2021 16:38, Brian Goetz wrote:

So, I think the "a switch only accepts null if the letters
n-u-l-l are present", while a comforting move in the short
term, buys us relatively little, and dulls our pain receptors
which in turn makes it take way longer to learn how patterns
really work.  I think we should go back to:

 - A switch accepts null if (a) one of the case labels is
`null` or (b) the switch has a total pattern (which must
always be the last case.) 


The proposal seems ok; it does nothing for the problem I'm
concerned about (e.g. type of the target expression changing and
influencing the totality analysis at a distance) - but that was
not address by the previous proposal either (as you say in your
email, admittedly, I was reading too much into your proposal).


At least, if you want a total type, you can make it explicit using
  case var x
which is always total whatever the type switched upon.

So you have two tools to avoid influence at distance in the totality 
analysis,
- for a switch where you can enumerate all the values enums, sealed 
type (boolean should be in that category too IMO, but we did not agree 
on that), if you list all the possible cases, a total case is not 
required.


Without changes to switch, there is nothing which would break if a "new 
case" is added (to the enum, or to the sealed hierarchy). So, listing 
"all possible cases" relies on the assumption that you know what "all 
cases" are. And right now there's no way to declaratively say: this 
switch (statement) is gonna cover them all. Brian answer goes a bit in 
that direction, which is good, for the outermost layer (but the problem 
still exists somewhat at the nested level).



- use "var" so the total case is explicit,  "case var x", "case 
Foo(var x)", etc
Sure - this is a good solution. One minor annoying thing is that we 
started from a position where we said "var is just for inference" and 
now we're back in a place where, while  var is still, conceptually at 
least, about inference, developers will also be using it for totality 
(as inference guarantees that you are always 100% covered).


Stepping back - my general feeling on this topic is that the
audience in this mailing list have a very intimate knowledge of
what a "total pattern" is, to the point that they are comfortable
building on top of this definition to e.g. define null behavior of
patterns. I'm a little afraid that the finer detail of totality
might be lost on the average Joe developer: totality is a much
more slippery concept than it seems. Sure, there is one obvious
way to make your pattern total: if the target expression has type
E, then add a type test pattern whose type is also E. That seems
easy enough. Except that, the type of E will not always be that
manifest in user code (e.g. might be the result of what javac
happens to infer on Tuesdays). And, if you mix this with sealed
classes, it might be possible for a switch to go from total to
non-total, as new permitted subtypes are added to a sealed
hierarchy. These might all be all corner cases - but I think it's
this complexity which contributes to my "isn't this all too
subtle?" feeling.

Obviously I'm well aware that nearly every path has been explored,
and no silver bullet seems to be laying around, so... this might
just be the best we can offer, and that's ok.


We tried to have a way to signal that a pattern is total or not, by 
example, using a keyword, like total or default, but it did not work 
well when a pattern is partially total like "case Foo(true, var x)"


Yep - I'm aware of the various roads not taken - I'm not suggesting that 
there's some shiny great solution which is better than what is being 
proposed; I just wanted to air my concerns about the complexity of the 
programming model implied in this proposal. In other cases (DA/DU, 
scoping of pattern variables and, to a certain degree type inference, 
esp. after Java 8) the rules are mind-blowingly complex, but developers 
can form an intuitive notion of how these things work, and trust the 
compiler to do the right thing - e.g. these features, despite their 
complexity are mostly out of your face, and when the compiler barks, the 
user will have some idea of what went wrong (whooops, uninitialized 
final variable here!). Totality analysis is not as comple

Re: Switch labels (null again), some tweaking

[Brian Goetz]

- for a switch where you can enumerate all the values enums, sealed 
type (boolean should be in that category too IMO, but we did not agree 
on that), if you list all the possible cases, a total case is not 
required.


In fact, when you can enumerate the values/types, it is better to _not_ 
have a catch-all.  Because then you get better type checking when you 
only think you listed them all, or a new one is added later.

Re: Switch labels (null again), some tweaking

[Remi Forax]

> De: "Maurizio Cimadamore" 
> À: "Brian Goetz" , "amber-spec-experts"
> 
> Envoyé: Mardi 27 Avril 2021 16:23:20
> Objet: Re: Switch labels (null again), some tweaking

> On 23/04/2021 16:38, Brian Goetz wrote:

>> So, I think the "a switch only accepts null if the letters n-u-l-l are 
>> present",
>> while a comforting move in the short term, buys us relatively little, and 
>> dulls
>> our pain receptors which in turn makes it take way longer to learn how 
>> patterns
>> really work. I think we should go back to:

>> - A switch accepts null if (a) one of the case labels is `null` or (b) the
>> switch has a total pattern (which must always be the last case.)
> The proposal seems ok; it does nothing for the problem I'm concerned about 
> (e.g.
> type of the target expression changing and influencing the totality analysis 
> at
> a distance) - but that was not address by the previous proposal either (as you
> say in your email, admittedly, I was reading too much into your proposal).
At least, if you want a total type, you can make it explicit using 
case var x 
which is always total whatever the type switched upon. 

So you have two tools to avoid influence at distance in the totality analysis, 
- for a switch where you can enumerate all the values enums, sealed type 
(boolean should be in that category too IMO, but we did not agree on that), if 
you list all the possible cases, a total case is not required. 
- use "var" so the total case is explicit, "case var x", "case Foo(var x)", etc 

> Stepping back - my general feeling on this topic is that the audience in this
> mailing list have a very intimate knowledge of what a "total pattern" is, to
> the point that they are comfortable building on top of this definition to e.g.
> define null behavior of patterns. I'm a little afraid that the finer detail of
> totality might be lost on the average Joe developer: totality is a much more
> slippery concept than it seems. Sure, there is one obvious way to make your
> pattern total: if the target expression has type E, then add a type test
> pattern whose type is also E. That seems easy enough. Except that, the type of
> E will not always be that manifest in user code (e.g. might be the result of
> what javac happens to infer on Tuesdays). And, if you mix this with sealed
> classes, it might be possible for a switch to go from total to non-total, as
> new permitted subtypes are added to a sealed hierarchy. These might all be all
> corner cases - but I think it's this complexity which contributes to my "isn't
> this all too subtle?" feeling.

> Obviously I'm well aware that nearly every path has been explored, and no 
> silver
> bullet seems to be laying around, so... this might just be the best we can
> offer, and that's ok.
We tried to have a way to signal that a pattern is total or not, by example, 
using a keyword, like total or default, but it did not work well when a pattern 
is partially total like "case Foo(true, var x)" 

> Cheers
> Maurizio
Rémi 

Re: Switch labels (null again), some tweaking

[John Rose]

On Apr 27, 2021, at 9:39 AM, Brian Goetz 
mailto:brian.go...@oracle.com>> wrote:

Where I think we need to shore up the story is in "how do I turn on 
exhaustiveness checking for statement switches.”

Yes, the non-exhaustiveness of legacy switches turns out
to be a hiding place for bugs and misconceptions.  I do like
your proposal (in the other thread) of turning on
non-exhaustiveness by default for as many switches as
possible.  It would seem to help users think about their
code more clearly.  And putting “default: break” at the
bottom seems as reasonable ask:  Basically, it annotates
that switch as non-exhaustive, making the code easier
to reason about.  In fact, *all* switches become easier
to reason about, since the last case is always the fallback.

All that said, I hope we don’t run into cases where somebody
has written a switch that really looks good w/o a default,
and will look worse with one.  Surely someone will bring
such a breed of switch, eventually, to the Big Pet Show.

— John

Re: Switch labels (null again), some tweaking

[Brian Goetz]

You've put your finger on the fundamental stewardship challenge here.  
If we were never going to go any farther than "deconstruction patterns 
in switch", then we would surely do a "worse is better" hack which 
separates nullity from totality.  But, if we want deconstruction 
patterns (or Optional.of(var x), or array patterns, or collection 
patterns, or pattern assignment, or ...), we have to confront _nesting_, 
and nesting puts the connection between totality and target type and 
nullity right in your face.


But, Joe Java has not yet thought very much about nesting, so the answer 
that you get to when you work out all the details is ... 
counterintuitive.   As a result, we've been bombarded with (at varying 
levels of constructiveness) attempts to hide this complexity.  But at 
root, we have a choice: we can solve for the whole problem, or we can 
solve for the easy problems and make the hard ones even harder.  This is 
not an easy, or obvious, choice.


My claim is that to make pattern matching successful in Java, where we 
have to spend our "get users to think about something new" budget is 
totality.  And totality is relative to "what are you total on."


Where I think we need to shore up the story is in "how do I turn on 
exhaustiveness checking for statement switches."  We already have that 
for expression switches, and several of the holes you are worried that 
users will fall into come from the fact that the compiler is sometimes, 
but not always, type checking switches for exhaustiveness.


We've been struggling with whether there are "pattern switches" and 
"legacy switches", or whether we've fully generalized switch.  If the 
former is unavoidable, it might be possible to enforce totality checking 
on all but the legacy constant switches.  After all, totalizing an 
intentionally partial switch is simple: add a `default: break` clause.


Stepping back - my general feeling on this topic is that the audience 
in this mailing list have a very intimate knowledge of what a "total 
pattern" is, to the point that they are comfortable building on top of 
this definition to e.g. define null behavior of patterns. I'm a little 
afraid that the finer detail of totality might be lost on the average 
Joe developer: totality is a much more slippery concept than it seems. 
Sure, there is one obvious way to make your pattern total: if the 
target expression has type E, then add a type test pattern whose type 
is also E. That seems easy enough. Except that, the type of E will not 
always be that manifest in user code (e.g. might be the result of what 
javac happens to infer on Tuesdays). And, if you mix this with sealed 
classes, it might be possible for a switch to go from total to 
non-total, as new permitted subtypes are added to a sealed hierarchy. 
These might all be all corner cases - but I think it's this complexity 
which contributes to my "isn't this all too subtle?" feeling.


Obviously I'm well aware that nearly every path has been explored, and 
no silver bullet seems to be laying around, so... this might just be 
the best we can offer, and that's ok.


Cheers
Maurizio

Re: Switch labels (null again), some tweaking

[Maurizio Cimadamore]

On 23/04/2021 16:38, Brian Goetz wrote:
So, I think the "a switch only accepts null if the letters n-u-l-l are 
present", while a comforting move in the short term, buys us 
relatively little, and dulls our pain receptors which in turn makes it 
take way longer to learn how patterns really work.  I think we should 
go back to:


 - A switch accepts null if (a) one of the case labels is `null` or 
(b) the switch has a total pattern (which must always be the last case.) 


The proposal seems ok; it does nothing for the problem I'm concerned 
about (e.g. type of the target expression changing and influencing the 
totality analysis at a distance) - but that was not address by the 
previous proposal either (as you say in your email, admittedly, I was 
reading too much into your proposal).


Stepping back - my general feeling on this topic is that the audience in 
this mailing list have a very intimate knowledge of what a "total 
pattern" is, to the point that they are comfortable building on top of 
this definition to e.g. define null behavior of patterns. I'm a little 
afraid that the finer detail of totality might be lost on the average 
Joe developer: totality is a much more slippery concept than it seems. 
Sure, there is one obvious way to make your pattern total: if the target 
expression has type E, then add a type test pattern whose type is also 
E. That seems easy enough. Except that, the type of E will not always be 
that manifest in user code (e.g. might be the result of what javac 
happens to infer on Tuesdays). And, if you mix this with sealed classes, 
it might be possible for a switch to go from total to non-total, as new 
permitted subtypes are added to a sealed hierarchy. These might all be 
all corner cases - but I think it's this complexity which contributes to 
my "isn't this all too subtle?" feeling.


Obviously I'm well aware that nearly every path has been explored, and 
no silver bullet seems to be laying around, so... this might just be the 
best we can offer, and that's ok.


Cheers
Maurizio

Re: Switch labels (null again), some tweaking

[Remi Forax]

I just want to add that there is another possible semantics than having case 
null + total pattern as null acceptable pattern. 

We have based the semantics of pattern matching to the semantics of the cascade 
of if instanceof with an else at the end. 
There is another one, method calls [1], a switch like this 
switch(o) { 
case String s: 
case Object o: 
} 
can be seen as equivalent to the methods 
void m(String s) { ... 
void m(Object o) { ... 
with the switch being equivalent to a call to the method m. 

This semantics is equivalent to the cascade of instanceof apart in one 
scenario, when the value is null. 
A call to m(null) invokes m(String s), not m(Object). 

You may think that the method call semantics is not a good one because it can 
answer that no method are applicable or no method are more specific than the 
other, 
but those cases are not possible if the switch is total ... apart with null. 

If the value is null and we have a switch like this 
switch(o) { 
case String s: 
case Integer i: 
case Object o: 
} 
if we use the method call semantics, either "String s" or "Integer i" can be 
called, and given that none is more specific than the other. 

We can deviate from the original method call semantics by saying, let's take 
the first match, but in that case, it's just a different semantics, not an 
existing Java semantics. 

I don't like this semantics, because it will be surprising for anyone that null 
will be captured by the first case. I prefer null to be trapped by the total 
pattern at the end. 

Sadly, it means that there is no *obvious* semantics for null and that whatever 
we choose, it will not what some people expect. 

Rémi 

[1] https://docs.oracle.com/javase/specs/jls/se16/html/jls-15.html#jls-15.12 

> De: "Brian Goetz" 
> À: "amber-spec-experts" 
> Envoyé: Vendredi 23 Avril 2021 17:38:42
> Objet: Re: Switch labels (null again), some tweaking

> Gavin has a spec that captures most of what we've talked about here, which
> should be posted soon. But I want to revisit one thing, because I think we may
> have swung a little too eagerly at a bad pitch.

> There is a distinction between the _semantics of a given pattern_ and _what a
> given construct might do with that pattern_. The construct (instanceof, 
> switch)
> gets first crack at having an opinion, and then may choose to evaluate whether
> the pattern matches something. The place where we have been most tempted to 
> use
> this flexibility is with "null", because null ruins everything.

> We made a decision to lump pattern matching in with `instanceof` because it
> seemed silly to have two almost identical but subtly different constructs for
> "dynamic type test" and "pattern match" (given that you can do dynamic type
> tests with patterns.) We knew that this would have some uncomfortable
> consequences, and what we have tentatively decided to do is outlaw total
> patterns in instanceof, so that users are not confronted with the subtle
> difference between `x instanceof Object` and `x instanceof Object o`. This may
> not be a totally satisfying answer, and we left some room to adjust this, but
> its where we are.

> The fact is that the natural interpretation of a total type pattern is that it
> matches null. People don't like this, partially because it goes against the
> intuition that's been built up by instanceof and switch. (If we have to, I'm
> willing to lay out the argument again, but after having been through it 
> umpteen
> times, I don't see any of the alternatives as being better.)

> So, given that a total type pattern matches null, but legacy switches reject
> null...

> The treatment of the `null` label solves a few problems:

> - It lets people who want to treat null specially in switch do so, without
> having to do so outside the switch.
> - It lets us combine null handling with other things (case null, default:), 
> and
> plays nicely when those other things have bindings (case null, String s:).
> - It provides a visual cue to the reader that this switch is nullable.

> It is this last one that I think we may have over-rotated on. In the treatment
> we've been discussing, we said:

> - switch always throws on null, unless there's a null label

> Now, this is clearly appealing from a "how do I know if a switch throws NPE or
> not" perspective, so its understandable why this seemed a clever hack. But
> reading the responses again:

> Tagir:
> > I support making case null the only null-friendly pattern.

> Maurizio:
> > there's no subtle type dependency analysis which determines the fate of null

> it seems that people wanted to read way more into this than there was; they
> wanted this to be a statement about patterns, no

Re: [External] : Re: Switch labels (null again), some tweaking

[forax]

> De: "Brian Goetz" 
> À: "Remi Forax" , "John Rose" 
> Cc: "amber-spec-experts" 
> Envoyé: Vendredi 23 Avril 2021 22:38:41
> Objet: Re: [External] : Re: Switch labels (null again), some tweaking

> On 4/23/2021 4:25 PM, Remi Forax wrote:

>>> Bottom line:  Trust the users to choose how
>>> explicit to be with nulls.  More importantly,
>>> trust them with compositional notations.

>> That's a solution, we do nothing and trust users.
>> The other solution is to force users to explicit say that the pattern is 
>> total,
>> by example by asking to use 'var o' instead of 'Object o',
>> but we already discuss that and only me and Tagir were agreeing that it is a
>> good idea.

> Yes, this is what I meant by "move the distinction around." We could say that
> `var x` and `Object x` are different patterns; this is a sharp edge in one
> place (blows up the notion that `var` is just type inference.) We could say
> that `default` and `Object x` are different patterns (which is what I'm
> suggesting), which puts the sharp edge somewhere else -- it means that 
> people's
> notion of totality is polluted by historical chance. We could have different
> patterns for Object! and Object?, which is appealing in a "say what you mean"
> way, but which forces users to think about a corner case all the time.
For the record, I was proposing to disallow `Object o` as a total pattern (as 
we disallow instanceof Object o) instead of making `var x` and `Object x` two 
different patterns, 
well, it also can be seen as two different patterns with `Object o` being an 
invalid one. 

> Reasonable people can differ about which of these (or other) approach is best
> for Java, but it is not reasonable to believe that we can hide this
> distinction.

Yes ! 

Rémi 

Re: [External] : Re: Switch labels (null again), some tweaking

[John Rose]

On Apr 23, 2021, at 1:38 PM, Brian Goetz 
mailto:brian.go...@oracle.com>> wrote:



On 4/23/2021 4:25 PM, Remi Forax wrote:

Bottom line:  Trust the users to choose how
explicit to be with nulls.  More importantly,
trust them with compositional notations.


That's a solution, we do nothing and trust users.
The other solution is to force users to explicit say that the pattern is total, 
by example by asking to use 'var o' instead of 'Object o',
but we already discuss that and only me and Tagir were agreeing that it is a 
good idea.

Yes, this is what I meant by "move the distinction around."  We could say that 
`var x` and `Object x` are different patterns; this is a sharp edge in one 
place (blows up the notion that `var` is just type inference.)  We could say 
that `default` and `Object x` are different patterns (which is what I'm 
suggesting), which puts the sharp edge somewhere else -- it means that people's 
notion of totality is polluted by historical chance.  We could have different 
patterns for Object! and Object?, which is appealing in a "say what you mean" 
way, but which forces users to think about a corner case all the time.

Reasonable people can differ about which of these (or other) approach is best 
for Java, but it is not reasonable to believe that we can hide this distinction.

Making “default” the oddity feels like the safest
move, on several grounds:

- it’s localized to switch structure (and we can localize further to the end of 
the switch)
- it is visually clear (a different token from “case”)
- it carries a connotation of “old school” (fancy case labels are the future)

Re: Switch labels (null again), some tweaking

[John Rose]

On Apr 23, 2021, at 1:10 PM, Brian Goetz 
mailto:brian.go...@oracle.com>> wrote:

I think the concern on the part of the null-fearers is not so much the O(n) 
scan (though that's a concern), as much as the subtle difference between `case 
Object o` and `default`.  They are almost identical, except in null.  No one 
likes having to carry that distinction around in their head.

I mildly disagree with this last point:  I think that
distinction will cause mild pain to learn, and zero
point zero zero pain to carry around for the rest
of one’s career.  I can feel the rule growing in my
own head: “default means old-school null rejection,
a null case label means null acceptance, if both
are present the null case label of course wins.”

Could this explicit null-ing be MaKing the New
nUlls Stand Out?

— John

Re: [External] : Re: Switch labels (null again), some tweaking

[Brian Goetz]

On 4/23/2021 4:25 PM, Remi Forax wrote:

Bottom line:  Trust the users to choose how
explicit to be with nulls.  More importantly,
trust them with compositional notations.

That's a solution, we do nothing and trust users.
The other solution is to force users to explicit say that the pattern is total, 
by example by asking to use 'var o' instead of 'Object o',
but we already discuss that and only me and Tagir were agreeing that it is a 
good idea.


Yes, this is what I meant by "move the distinction around."  We could 
say that `var x` and `Object x` are different patterns; this is a sharp 
edge in one place (blows up the notion that `var` is just type 
inference.)  We could say that `default` and `Object x` are different 
patterns (which is what I'm suggesting), which puts the sharp edge 
somewhere else -- it means that people's notion of totality is polluted 
by historical chance.  We could have different patterns for Object! and 
Object?, which is appealing in a "say what you mean" way, but which 
forces users to think about a corner case all the time.


Reasonable people can differ about which of these (or other) approach is 
best for Java, but it is not reasonable to believe that we can hide this 
distinction.

Re: Switch labels (null again), some tweaking

[Remi Forax]

- Mail original -
> De: "John Rose" 
> À: "Brian Goetz" 
> Cc: "amber-spec-experts" 
> Envoyé: Vendredi 23 Avril 2021 21:27:40
> Objet: Re: Switch labels (null again), some tweaking

> On Apr 23, 2021, at 8:38 AM, Brian Goetz  wrote:
>> 
>> ...The fact is that the natural interpretation of a total type pattern is 
>> that
>> it matches null.  People don't like this…
> 
> This person does.  As you point out, this position
> enables composition of patterns.  And composition
> is the more important goal, compared to preservation
> of intuitions about edge cases.

I agree composition is more important, a total pattern should match null 
because semantically a total pattern is equivalent to "else" and not "if 
instanceof".

[...]

>> Now, let's look back at the alternative, where we keep the flexibility of the
>> null label, but treat patterns as meaning what they mean, and letting switch
>> decide to throw based on whether there is a nullable pattern or not.  So a
>> switch with a total type pattern -- that is, `var x` or `Object x` -- will
>> accept null, and thread it into the total case (which also must be the last
>> case.)
> 
> To me this is the material point, and has been all along:
> There is never a need to perform an O(N) visual scan of
> a switch to see if it accepts nulls, since the users simply
> have to inspect the final (and perhaps initial) case of the
> the switch.  Good style will avoid puzzlers such as final
> cases which are difficult to classify (total vs. partial).
> The language does not have to carry the burden of
> enforcing full annotation.
> 
> A second point:  In the present design, and especially
> with the cleanup you are proposing, I think there are
> several possible (optionally selectable) styles of
> null processing in switches.
> 
> (Reading later I see you already brought up most
> of these points.)
> 
> Style A1 is implicit null acceptance.  Pattern
> totality determines null acceptance, end of story.
> Style A2 is implicit null rejection, with markup
> of non-totality using `default`.  That is, a coder
> could choose, as a matter of clarity, to call out
> partial final cases by adding `default: break;`
> after them.  (E-switches don’t need A2.)
> 
> Style B1 is explicit null acceptance.  If null
> is allowed by the switch, then the token
> `null` must be present, either at the head
> of the switch or just before the final total
> pattern.  Style B2 adds explicit null rejection,
> by adding something like `case null: throw …`.
> That’s probably too much noise in most cases.
> 
> The current draft mandates explicit null
> acceptance.  Brian is suggesting that we
> allow the other style too.  I think it’s a
> good suggestion.
> 
> (An extra option would be to allow some
> bespoke way to annotate totality and/or
> non-totality of the final case. 

If we have a change to do, i'm not sure, i would prefer that option.
Make clear that the last pattern is total so it matches null.

> That interacts with things like enums and sealed classes,
> so I’ll just mention it and move on.)

???,
in those cases, no total pattern is needed, i don't see the interaction.

> 
> I think that IDEs can help users pick
> the style that is correct for them.
> 
> Bottom line:  Trust the users to choose how
> explicit to be with nulls.  More importantly,
> trust them with compositional notations.

That's a solution, we do nothing and trust users.
The other solution is to force users to explicit say that the pattern is total, 
by example by asking to use 'var o' instead of 'Object o',
but we already discuss that and only me and Tagir were agreeing that it is a 
good idea.

[...]

> 
> — John

Rémi

Re: Switch labels (null again), some tweaking

[Brian Goetz]

Now, let's look back at the alternative, where we keep the flexibility of the 
null label, but treat patterns as meaning what they mean, and letting switch 
decide to throw based on whether there is a nullable pattern or not.  So a 
switch with a total type pattern -- that is, `var x` or `Object x` -- will 
accept null, and thread it into the total case (which also must be the last 
case.)

To me this is the material point, and has been all along:
There is never a need to perform an O(N) visual scan of
a switch to see if it accepts nulls, since the users simply
have to inspect the final (and perhaps initial) case of the
the switch.  Good style will avoid puzzlers such as final
cases which are difficult to classify (total vs. partial).
The language does not have to carry the burden of
enforcing full annotation.


I think the concern on the part of the null-fearers is not so much the 
O(n) scan (though that's a concern), as much as the subtle difference 
between `case Object o` and `default`.  They are almost identical, 
except in null.  No one likes having to carry that distinction around in 
their head.


The essential point here is, though: that subtle distinction has to live 
somewhere; we don't get to banish it, we just get to try to put it where 
it does the least damage.  And the place that seems least damaging in 
the short run, is likely more damaging in the long run.


(I am starting to think I should rethink Serialization's position as my 
"most regretted feature", given the degree to which null distorts every 
language evolution discussion)

Re: Switch labels (null again), some tweaking

[John Rose]

On Apr 23, 2021, at 8:38 AM, Brian Goetz  wrote:
> 
> ...The fact is that the natural interpretation of a total type pattern is 
> that it matches null.  People don't like this…

This person does.  As you point out, this position
enables composition of patterns.  And composition
is the more important goal, compared to preservation
of intuitions about edge cases.


> 
> So, given that a total type pattern matches null, but legacy switches reject 
> null...
> 
> The treatment of the `null` label solves a few problems:
> 
>  - It lets people who want to treat null specially in switch do so, without 
> having to do so outside the switch.  

Re. composition, it lets the switch be refactored into smaller
or larger switches while still managing its own business.
No need to bring in extra `if` statements.

>  - It lets us combine null handling with other things (case null, default:), 
> and plays nicely when those other things have bindings (case null, String s:).
>  - It provides a visual cue to the reader that this switch is nullable.  
> 
> It is this last one that I think we may have over-rotated on.

I’m glad you are bringing this up. 

> In the treatment we've been discussing, we said:
> 
>  - switch always throws on null, unless there's a null label
> 
> Now, this is clearly appealing from a "how do I know if a switch throws NPE 
> or not" perspective, so its understandable why this seemed a clever hack.

I agree with this goal, as a secondary goal.  But the
hack is not clever if it harms a more important goal.


>   ...It might be better to rip the band-aid off, and admit how patterns work.

(Because that’s the place Java will be in the long run.)

> Here's an example of the kind of mistake that this treatment encourages.

Good example.

>   ...The first switch does the right thing; the second will NPE on Foo(null). 
>  And by insulating people from the real behavior of type patterns, it will be 
> even more surprising when this happens.  

It’s possible to tweak the code to work around
the problem by adding `null,` on the last case.
And an IDE could do this.  But it’s a sharp edge
that comes from the extra interference of `switch`
into pattern semantics, which harms the primary
goal of composition.

> Now, let's look back at the alternative, where we keep the flexibility of the 
> null label, but treat patterns as meaning what they mean, and letting switch 
> decide to throw based on whether there is a nullable pattern or not.  So a 
> switch with a total type pattern -- that is, `var x` or `Object x` -- will 
> accept null, and thread it into the total case (which also must be the last 
> case.) 

To me this is the material point, and has been all along:
There is never a need to perform an O(N) visual scan of
a switch to see if it accepts nulls, since the users simply
have to inspect the final (and perhaps initial) case of the
the switch.  Good style will avoid puzzlers such as final
cases which are difficult to classify (total vs. partial).
The language does not have to carry the burden of
enforcing full annotation.

A second point:  In the present design, and especially
with the cleanup you are proposing, I think there are
several possible (optionally selectable) styles of
null processing in switches.

(Reading later I see you already brought up most
of these points.)

Style A1 is implicit null acceptance.  Pattern
totality determines null acceptance, end of story.
Style A2 is implicit null rejection, with markup
of non-totality using `default`.  That is, a coder
could choose, as a matter of clarity, to call out
partial final cases by adding `default: break;`
after them.  (E-switches don’t need A2.)

Style B1 is explicit null acceptance.  If null
is allowed by the switch, then the token
`null` must be present, either at the head
of the switch or just before the final total
pattern.  Style B2 adds explicit null rejection,
by adding something like `case null: throw …`.
That’s probably too much noise in most cases.

The current draft mandates explicit null
acceptance.  Brian is suggesting that we
allow the other style too.  I think it’s a
good suggestion.

(An extra option would be to allow some
bespoke way to annotate totality and/or
non-totality of the final case.  That interacts
with things like enums and sealed classes,
so I’ll just mention it and move on.)

I think that IDEs can help users pick
the style that is correct for them.

Bottom line:  Trust the users to choose how
explicit to be with nulls.  More importantly,
trust them with compositional notations.


>  Who is this going to burn, that is not going to be burned by the existing 
> switch behavior anyway?  I think very, very few people.  To get burned, a lot 
> of things have to come together.  People are used to saying `default`; those 
> that continue to are not going to get burned.

(Style A2.)

>   People are generally in agreement that `var x` should be total; people who 
> use that are not going to get burned.  Switches today NPE eagerl

Re: Switch labels (null again), some tweaking

[Brian Goetz]

Gavin has a spec that captures most of what we've talked about here, 
which should be posted soon.  But I want to revisit one thing, because I 
think we may have swung a little too eagerly at a bad pitch.


There is a distinction between the _semantics of a given pattern_ and 
_what a given construct might do with that pattern_.  The construct 
(instanceof, switch) gets first crack at having an opinion, and then may 
choose to evaluate whether the pattern matches something.  The place 
where we have been most tempted to use this flexibility is with "null", 
because null ruins everything.


We made a decision to lump pattern matching in with `instanceof` because 
it seemed silly to have two almost identical but subtly different 
constructs for "dynamic type test" and "pattern match" (given that you 
can do dynamic type tests with patterns.)  We knew that this would have 
some uncomfortable consequences, and what we have tentatively decided to 
do is outlaw total patterns in instanceof, so that users are not 
confronted with the subtle difference between `x instanceof Object` and 
`x instanceof Object o`.  This may not be a totally satisfying answer, 
and we left some room to adjust this, but its where we are.


The fact is that the natural interpretation of a total type pattern is 
that it matches null.  People don't like this, partially because it goes 
against the intuition that's been built up by instanceof and switch.  
(If we have to, I'm willing to lay out the argument again, but after 
having been through it umpteen times, I don't see any of the 
alternatives as being better.)


So, given that a total type pattern matches null, but legacy switches 
reject null...


The treatment of the `null` label solves a few problems:

 - It lets people who want to treat null specially in switch do so, 
without having to do so outside the switch.
 - It lets us combine null handling with other things (case null, 
default:), and plays nicely when those other things have bindings (case 
null, String s:).

 - It provides a visual cue to the reader that this switch is nullable.

It is this last one that I think we may have over-rotated on. In the 
treatment we've been discussing, we said:


 - switch always throws on null, unless there's a null label

Now, this is clearly appealing from a "how do I know if a switch throws 
NPE or not" perspective, so its understandable why this seemed a clever 
hack.  But reading the responses again:


Tagir:
> I support making case null the only null-friendly pattern.

Maurizio:
> there's no subtle type dependency analysis which determines the fate 
of null


it seems that people wanted to read way more into this than there was; 
they wanted this to be a statement about patterns, not about switch.  I 
think this is yet another example of the "I hate null so much I'm 
willing to take anything to make it (appear to) go away" biases we all 
have."  Only Remi seemed to have recognized this for the blatant trick 
it is -- we're hiding the null-accepting behavior of total patterns 
until people encounter them with nested patterns, where it will be less 
uncomfortable.


To be clear: this is *not* making `null` the only null-friendly 
pattern.  But these responses make me worry that, if the experts can't 
tell the difference, then no user will be able to tell the difference, 
and that this is just kicking the confusion down the road.  It might be 
better to rip the band-aid off, and admit how patterns work.


Here's an example of the kind of mistake that this treatment 
encourages.  If we have:


    switch (x) {
    case Foo(String a):  A
        case Foo(Integer a): B
    case Foo(Object a):  C
    }

and we want to refactor to

switch (x) {
    case Foo(var a):
        switch(a) {
    case String a:  A
    case Integer a: B
    case Object a:  C
    }
    }

we've made a mistake.  The first switch does the right thing; the second 
will NPE on Foo(null).  And by insulating people from the real behavior 
of type patterns, it will be even more surprising when this happens.


Now, let's look back at the alternative, where we keep the flexibility 
of the null label, but treat patterns as meaning what they mean, and 
letting switch decide to throw based on whether there is a nullable 
pattern or not.  So a switch with a total type pattern -- that is, `var 
x` or `Object x` -- will accept null, and thread it into the total case 
(which also must be the last case.)


Who is this going to burn, that is not going to be burned by the 
existing switch behavior anyway?  I think very, very few people.  To get 
burned, a lot of things have to come together.  People are used to 
saying `default`; those that continue to are not going to get burned.  
People are generally in agreement that `var x` should be total; people 
who use that are not going to get burned.  Switches today NPE eagerly on 
null, so having a null flow into code that doesn't ex