What's the theoretical difference between this kind of pattern matching and polymorphism? Instead of encoding the logic for each branch in a switch, do we get the same kind of exhaustive static guarantees if instead we encode each branch as a polymorphic implementation on each type?
For example, Java's Optional type seems to provide the same static guarantees without pattern matching (assuming it didn't have the unsafe get() method).
You are right assuming the more or less equality between two approaches.
For example, you can encode Just as fJust :: a -> (a -> b) -> b and Nothing as fNothing :: b -> b. fJust receives a computation that accepts argument of Just constructor, while fNothing receives just a value to be returned. Or, alternatively, you can look at the type of maybe function which is pattern matching on Maybe in disguise: maybe :: b -> (a -> b) -> Maybe a -> b.
(I believe this method is called Church encoding)
But when you go from structure of types and patterns to functions, you lose the ability of analysis (of exhaustivity or anything else). You now deal with something that is Turing complete instead of fixed size structure.
And this is delimition of "possible" and "impossible". With the Church encoding analysis of matching completeness is impossible and even writing matchers for lists or trees is nigh to impossible, actually.
i think they're considered two sides of the same coin - exhaustive vs extensible, each with its benefits and tradeoffs. this is known as "The Expression Problem"; what follows is a quick and messy intro.
sum types:
you can easily add new functions that accept your sum type, but adding a new "variant" to the type will require modifying every function you've written to support the new case
polymorphism (interfaces):
you can easily add new types that implement your interface, but if you want to add a new method/function to it, you're going to have to implement it for every type that implements your interface
essentially, we've got two "extensibility dimensions": one for adding new operations, and one for adding new types. sum types are good on the operation axis, interfaces are good on the type axis. (it's an open research question if there's a solution that's good on both.) i hope this makes sense!
as a side note, when discussing this, it's useful to distinguish ad-hoc polymorphism (subclassing, interfaces/typeclasses) and parametric polymorphism (generics) – here, we're talking about the "ad-hoc" variety. I mention this because i saw some confusion about this in a sibling thread but can't reply there.
Javas optional type was directly inspired by scala and haskell. The concept is the same. However, because java doesn't have pattern matching as a feature internally it is implemented as a design pattern.
Haskell's implementation of "match" is so elegant that it will take you a while to realize that the "exhaustive" pattern matching is a big part of what is contributing to haskells safety.
I've used pattern matching languages quite a bit (in my case, it's OCaml), so I know what it's like. I'm just curious if there's any fundamental difference between pattern matching and polymorphism. From a cursory glance, it seems like they can statically prove the same properties about programs and are equivalent from that perspective.
If that's the case, then the conversation shifts from "you should use pattern matching" to "when should I use pattern matching?" Which is a pretty interesting question. Logic locality seems to be an obvious criteria (does the logic live with the type, or with the consumer of the type?).
I'm not clear what you're asking here. It sounds to me your asking the difference between a table and a chair.
Pattern matching is syntactic sugar for extracting values from a pattern. In a statically typed language the compiler has the option of forcing the user to handle every possible type permutation with a pattern thus ensuring safety.
Polymorphism is just a generic type.
That's as far as I know... could you elaborate more on what you mean?
For example, Java's Optional type seems to provide the same static guarantees without pattern matching (assuming it didn't have the unsafe get() method).