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 <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/aa4d0950/attachment.htm>