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!

1 Like

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

11 Likes

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,

1 Like

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

1 Like