Switch labels (null again), some tweaking
Maurizio Cimadamore
maurizio.cimadamore at oracle.com
Wed Apr 28 21:34:51 UTC 2021
Thanks for this.
It is especially helpful to see all the rules in a single place.
So, armed with these rules - back to the first example I brought up:
switch (lunch) {
case Box(Soup s) {
if (s == null) {
System.err.println("Box of null");
} else {
System.err.println("Box of soup");
}
}
case Bag(Soup s): {
if (s == null) {
System.err.println("Bag of null");
} else {
System.err.println("Bag of soup");
}
}
}
If I read the rules correctly, Box(Soup) + Bag(Soup) "cover"
Container<Lunch>, with the exception of the { null, Box(null), Bag(null)
}. So the above will throw when `lunch` is null, and will also throw
with Box(null) or Bag(null). Correct?
So the right way to write that would be to add a couple of { case
Box(null), case Bag(null) } - these will reduce the remainder of the
switch blanket to just { null } - which means the switch will just throw
on a null input value, as usual.
Assuming I got it correct, I think that if we can get javac to spit out
all the elements in the remainder (as in the list I wrote above), then
it should be possible for users to understand what's going wrong, and
how to fix it.
Maurizio
On 28/04/2021 21:11, Brian Goetz 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.
>>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20210428/fbf845bc/attachment-0001.htm>
More information about the amber-spec-experts
mailing list