How does the compiler check for exhaustive pattern matching?

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.

Thank you in advance!

The canonical reference for exhaustivity-checking in OCaml is the scientific publication

Warnings for pattern matching
Luc Maranget
2007

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.)

A question:
F# has the “OR pattern” (pattern1 | pattern2) but also an “AND pattern” (pattern1 & pattern2).
Pattern Matching

Any equivalent for OCaml?

No, but you can use when guards and as binds to implement some of them, e.g., F# pattern (x,y) & (_,"hello") could be encoded in OCaml as

  • (x, "hello" as y) or as
  • (x,y) when y = "hello".

See also,

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).