Switch labels (null again), some tweaking

[Brian Goetz]

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

The pattern Box(Soup) on its own is total on Box<Soup> (as opposed to 
Box<Lunch>), 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<Lunch> 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
>
>
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20210428/e942e9cd/attachment-0001.htm>