# How does the compiler check for exhaustive pattern matching? **URL:** \ **Category:** Learning\ **Tags:** compiler\ **Created:** [January 14, 2020, 3:21pm UTC](https://discuss.ocaml.org/t/how-does-the-compiler-check-for-exhaustive-pattern-matching/5013 "2020-01-14T15:21:17Z")\ **Posts on this page:** 5\ **Page:** 1
**Author:** ![dylanirlbeck](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/dylanirlbeck/32/1941_2.png) [@dylanirlbeck](https://discuss.ocaml.org/u/dylanirlbeck)\ **Post date:** [January 14, 2020, 3:21pm UTC](https://discuss.ocaml.org/t/how-does-the-compiler-check-for-exhaustive-pattern-matching/5013/1 "2020-01-14T15:21:17Z")
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! ---
**Author:** ![gasche](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gasche/32/4_2.png) [@gasche](https://discuss.ocaml.org/u/gasche)\ **Post date:** [January 14, 2020, 3:59pm UTC](https://discuss.ocaml.org/t/how-does-the-compiler-check-for-exhaustive-pattern-matching/5013/2 "2020-01-14T15:59:34Z")
The canonical reference for exhaustivity-checking in OCaml is the scientific publication > [Warnings for pattern matching](http://moscova.inria.fr/~maranget/papers/warn/index.html) > 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.) ---
**Author:** ![spop](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/spop/32/797_2.png) [@spop](https://discuss.ocaml.org/u/spop)\ **Post date:** [January 14, 2020, 5:35pm UTC](https://discuss.ocaml.org/t/how-does-the-compiler-check-for-exhaustive-pattern-matching/5013/3 "2020-01-14T17:35:08Z")
A question: F# has the “OR pattern” (pattern1 | pattern2) but also an “AND pattern” (pattern1 & pattern2). [Pattern Matching](https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/pattern-matching) Any equivalent for OCaml? ---
**Author:** ![ivg](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ivg/32/103_2.png) [@ivg](https://discuss.ocaml.org/u/ivg)\ **Post date:** [January 14, 2020, 7:02pm UTC](https://discuss.ocaml.org/t/how-does-the-compiler-check-for-exhaustive-pattern-matching/5013/4 "2020-01-14T19:02:06Z")
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, > [@Musings on extended pattern-matching syntaxes](https://discuss.ocaml.org/t/musings-on-extended-pattern-matching-syntaxes/3600): > > Hello Discourse, I thought it might be amusing to share two ideas for extending OCaml’s pattern-matching syntax. (I don’t plan to implement them for now because technically it would be difficult.) with-patterns using and Agda has [with abstractions](https://agda.readthedocs.io/en/v2.5.4.2/language/with-abstraction.html), which allow to start, in the middle of a pattern-matching, to further match on the value of an expression: filter\_map : {A B : Set} → (A → Maybe B) → List A → List B filter\_map f [] = [] filter f (x ∷ xs) with f x filter f (x ∷ xs) | Some y =… ---
**Author:** ![gasche](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gasche/32/4_2.png) [@gasche](https://discuss.ocaml.org/u/gasche)\ **Post date:** [January 14, 2020, 8:26pm UTC](https://discuss.ocaml.org/t/how-does-the-compiler-check-for-exhaustive-pattern-matching/5013/5 "2020-01-14T20:26:47Z")
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).