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