I like “covers” better than the best phrase I came up with, which was
“ostensibly exhaustive”. :-)
This looks like a good recap.
—Guy
> On Apr 28, 2021, at 4:11 PM, Brian Goetz <brian.go...@oracle.com> wrote:
>
> 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.
>>>>
>>>>
>>>>
>>
>
