Hi all. I’m relatively new to OCaml, and I was curious on how the compiler is able to give a warning when a case list is non-exhaustive - both from a high-level and, if possible, the implementation of this check. I have some ideas about how one could do this, but none of my ideas seem like they’d be nearly as efficient as the OCaml compiler is.
The general idea is to consider all the patterns of a given pattern-matching at once, generalize this structure to a “matrix” of patterns (matching on several values in parallel), and devise an algorithm to “explore” these pattern matrices in such a way that you eventually tell if a given pattern-matrix is exhaustive, or can propose a counter-example.
(I guess we should write a high-level/accessible blog post about this.)
We could in fact generalize p1 as x into p1 as p2 to support general pattern intersection, but I’ve been waiting to do more work on cleaning up the pattern-matching implementation before trying to implement this (it’s probably not very difficult, but it’s a good piece of work).