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<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.

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<Soup> must have been total on 
Box<Lunch> (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<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/65ac37cb/attachment-0001.htm>