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 <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/1fb4d760/attachment-0001.htm>