Next up for patterns: type patterns in switch

[Brian Goetz]

>> 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.  

> 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..  

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 clases
 - 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.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200813/353ec0b5/attachment-0001.htm>