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.
