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.
Starting with the second definition of the function non-triv-pat-p (the real definition which replaces the temporary stub one), the module starts to eat its own dogfood by using its own pattern matching.
That function, for instance, decides whether a pattern is "trivial" or not, using pattern matching itself on the pattern matching notation.
The string quasiliteral pattern's expansion relies heavily on pattern matching, also.
Thanks for writing! Love the composition of your site pages btw. I've got the same "|"-seperated nav bar on my WIP branch. Cleaner then my current branch, but I'm trying to compromise between sparse-ness and something with more "vibes". If only I was in the habit of actually writing anything-- congats!
