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 <total pattern>` 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<Boolean> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20210428/b7c70bd3/attachment-0001.htm>