A (IMHO) good and easy to read introduction is Wadler's "EFFICIENT COMPILATION OF PATTERN-MATCHING", chapter 5 of "The Implementation of Functional Programming Languages" https://simon.peytonjones.org/assets/pdfs/slpj-book-1987-2up... - actually I can recommend the whole book as an instruction to (the interesting stuff of) writing a compiler for a functional language. It also contains an introduction to the lambda calculus.

If you are interested, I wrote a thesis in 2007 on "object-oriented pattern matching" available at EPFL which "formalizes" pattern matching in Scala. It did not get into path-dependent types and does not have mechanized proofs, but has a discussion of optimizing translation to lower level code, exhaustiveness checks and user definable patterns (extractors). Like the author of the article, I found Maranget's matrix representation a great basis. This is because algebraic data types come in the form of "sum of products" (or enums with records) and once you have tested one level you want to expand the components of the tuple pattern (columns) and you deal with multiple cases (rows).

I won't claim my thesis is the most readable. I think I would do the presentation very differently today, but going back one's theis topic seems to be one of these impossible things in life if you don't work in academia.

Fun to see. When I worked on the implementation of Rod Burstall’s HOPE language (https://dl.acm.org/doi/pdf/10.1145/800087.802799) in 1979 I “invented” pattern compilation and implemented it (in POP-2) for the HOPE interpreter. HOPE patterns were of course way simpler than Haskell patterns, so my algorithm was pretty straightforward. From the math point of view, any function or arity n that has a parameter whose possible actual values belong to a finite discrete set can be replaced by a family of functions of arity n-1.

Something as simple as "is this string in this fixed set of strings" benefits from compile-time optimization of the matching algorithm. This is a place where Lisp's macros really shine, as they enable this kind of optimization to be performed at macro expansion time, without the need for preprocessing or matching algorithms built into the compiler itself.

https://www.cs.tufts.edu/~nr/cs257/archive/norman-ramsey/mat... by the current Microsoft CTO

This is my blog, thanks for posting - never expected to see such engagement.

IIRC luc maranget's paper was also a basis to clojure/script core.match

ps: checked https://github.com/clojure/core.match/wiki/References