Next up for patterns: type patterns in switch

[forax at univ-mlv.fr]

> De: "Brian Goetz" <brian.goetz at oracle.com>
> À: "Guy Steele" <guy.steele at oracle.com>
> Cc: "Remi Forax" <forax at univ-mlv.fr>, "John Rose" <john.r.rose at oracle.com>,
> "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Jeudi 13 Août 2020 16:24:11
> Objet: Re: Next up for patterns: type patterns in switch

>>> I agree destructuring is just as important as conditionality and those two
>>> things should be orthogonal.
>>> But i still think having a keyword to signal that a pattern (not a case) is
>>> total is better than letting people guess.

> I’m glad this discussion has moved to the right thing — whether we should
> provide extra help in type-checking totality. (Note, though, there were several
> dozen aspects to my patterns-in-switch proposal, and we’ve spent 99% of our
> time discussing a single, pretty cornery one. This is the hazard of discussing
> these things on mailing lists, where all the discussion is replies to the first
> thing that someone complained about, especially when the first complaint is
> loud. So EVERYONE, PLEASE, take a detailed review through the doc. It can’t be
> 100% perfect aside form this issue.)

> I still think, though, that this may be mostly fear of the unknown. Having spent
> the last year staring at pattern switches, it is really pretty obvious which
> are the total ones. I think that will be true for most users, once they use the
> feature a little. (Remember how alien people said method references looked, or
> how worried people were about the fact that static mrefs and unbound instance
> mrefs had the same syntax? Wasn’t a problem.) So all of this discussion rests
> on the assumption that (a) it is really hard to tell when a pattern is total or
> not, and (b) the stakes for getting that wrong are really high. I worry that
> both of these concerns are significantly overstated, and that the incremental
> user model complexity may be worse than the disease.

I'm still not sure that using a keyword to mark that a pattern is total is the best solution, i still like the rule that a total pattern should use var, it's less intrusive but perhaps i've written too much OCAML so i've no problem with all types being inferred in a pattern matching. 

If you are doing pattern matching on a hierarchy you have not built yourself, it's quite easy to think that a pattern a total while it's not. 
As an anecdote, in the example with TadPole, i did not now what a tadpole was (why on earth you have two words for a pollywog in English ?) so the relation between a Frog and a TadPole was not that clear for me. 

And given that the semantics is different when a pattern is total or not, i think a syntactic difference do more good than harm. 

>> Yes, and here is the example that convinced me that one needs to be able to mark
>> patterns as total, not just cases:

> The underlying observation here is that totality is a property of an arbitrary
> sub-tree of a pattern, which could be the whole thing, a leaf, or some
> intermediate sub-tree.

> Guy’s exploration into overloading `default` does shine a light on one of the
> uglier parts of my proposal, which is that the existing `default` case is
> mostly left to rot. I’m going to take this as a cue that, whether we do
> something to highlight pattern totality or not, that we should try to integrate
> default cases better into the design.

> So, here are the properties of the existing default case, in the current state
> of the proposal:

> - it matches all non-null values with no bindings
> - it can only appear at the end (unlike the current language, where it can
> appear anywhere)
> - You cannot fall into it from a pattern case (unlike the current language,
> where you can fall into it)
> - People will either use default or a total pattern, but rarely both (since
> their only difference is null)

> Just as we’ve leaned towards rehabilitating switch, maybe we can try to
> rehabilitate default. And the role it can play is in signaling totality of the
> switch.

yes 

> There are two “cases” of exhaustive switches: nullable ones and non-nullable
> ones.

> The nullable ones are those that end in a total (catch-all) pattern. The
> non-nullable ones are the analogues of the current exhaustive switch on enums;
> those where all the cases are “parts” of the whole:

> switch (day) {
> case MONDAY..FRIDAY: work();
> case SATURDAY: play();
> case SUNDAY: worship();
> // And on the null day, there was a NullPointerException
> }

> This is a total switch, but not a nullable one. On the other hand:

> switch (something) {
> case X: ...
> case Object o:
> }

> This is also a total switch, but a nullable one.

> So here’s a proposed rehabilitation of default, inspired by Guy’s exploration:

> - A switch has a sequence of cases, with zero or one default case
> - The default case must be last (except for legacy switches)
> - A switch with a default case must be total (possibly modulo null)
> - Default can be used with no pattern, which means “everything else but null”
> - Default can be used with a pattern, in which case it has exactly the same
> semantics as the same pattern with “case”
> - Nullability is still strictly a function of whether there are any nullable
> cases, which can only be “case null” (first) and total pattern (last)

> So we can say

> switch (something) {
> case X: ...
> case Object o:
> }

> or

> switch (something) {
> case X: ...
> default Object o:
> }

> which mean the same thing, but the latter engages the additional type checking
> that the switch is total.

> This is not inconsistent with GUy’s sketch, it just is the switch-specific part.

I think you know my position on this, i would prefer the compiler to emit an error on the former code and ask to add default, converting the former code to the latter. 

The current status quo is a way to be sure that people will talk endlessly about that, with the "pro" default advocating for more safety while the others will answer that seeing if a pattern is total or not is obvious and it's less keystrokes. 

Rémi 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200814/2c1f183c/attachment-0001.htm>