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.
