New pattern matching doc

Brian Goetz brian.goetz at oracle.com
Fri Jan 8 16:26:33 UTC 2021


> Here is another example that propose a way to declare that several 
> case methods are total using the keyword exclusive
> (if one case method is marked exclusive, all case methods must be 
> marked exclusive).

The document alludes to this problem; certain sets of patterns are, in 
aggregate, total on a type.  The poster child is `Optional.of` and 
`Optional.empty`.  And yes, we want a way to express totality in the 
model (though, since we haven't even gotten to the mechanics of 
static/instance patterns yet, this is even further down the list). F# 
does it in the pattern declaration; somewhere there is a declaration 
like "pattern Foo = Bar | Baz", which captures the sum-ness of them.

Your `MyNumber` example induces a sum by saying "all the patterns in 
this class."  This works in theory, but I think this particular approach 
runs out of gas pretty quickly, since (for example) a class could easily 
have patterns that are not part of the sum.  (Further, patterns can 
overlap; I can have patterns for a, b, and a|b, and _any two_ of them 
are total.)

Again, I think this is a little farther down the road, but I think the 
winning intuition here is to synthesize exhaustiveness by constructively 
demonstrating adjunction to a known sealed domain. For example, Optional 
is adjoint to Boolean; if we project Optional down to Boolean, saying 
that the `Optional.of` pattern corresponds to true and the 
`Optional.empty` pattern corresponds to `false`, then we can derive both 
exhaustiveness _and more efficient dispatch_ from this information.  
Similarly, the Javac tree classes have `Kind` enums, and enums are 
sealed, so if we can project patterns down to (sets of) kinds, then the 
compiler can again derive both exhaustiveness and more efficient 
dispatch.  (All this is to say that, while I don't have a 100% 
bulletproof answer yet, I've spent quite a bit of time on it, and 
already rejected the first six naive ideas here.)

What I take from your mail here is "exhaustiveness is important"; I 
agree (and said as much in the doc.)  Is there more, that I've missed?



More information about the amber-spec-experts mailing list