Warnings for pattern matching

✨ Summary

Overview

The paper gives a semantic and algorithmic treatment of two common pattern-matching anomalies: non-exhaustive matches, where some values are not covered, and useless clauses, where a clause can never be selected because earlier clauses already cover all of its instances. The central abstraction is usefulness: a pattern is useful with respect to a matrix of preceding patterns if there exists a value matched by the pattern but by none of the preceding rows.

The proposed algorithm, generally referred to as algorithm U, recursively analyzes pattern matrices using constructor specialization and default matrices. It determines both exhaustiveness and clause usefulness without constructing a potentially exponential decision tree. The paper proves that the same algorithm is correct under strict ML semantics, a general class of lazy matching semantics, Laville’s incompatibility-based semantics, and Haskell’s left-to-right matching semantics.

The implementation extends the basic analysis in two important ways. First, algorithm I produces a pattern representing a counterexample when a match is non-exhaustive. Second, algorithm U′ analyzes individual alternatives inside or-patterns, allowing compilers to warn about partially useless patterns rather than merely reporting that an entire clause is useful or useless. The implementation also applies safeguards based on subsumption and incompatibility to reduce the risk of exponential behavior. Measurements reported for the Objective Caml compiler indicate that the analysis adds relatively little compilation overhead on ordinary programs, while the safeguards substantially improve behavior for selected difficult inputs.

Influence and subsequent use

The work directly influenced compiler practice. The OCaml community identifies it as the canonical reference for the compiler’s exhaustiveness and usefulness checks. (discuss.ocaml.org) Rust’s compiler documentation states that its pattern-analysis implementation is inspired by Maranget’s algorithm and uses the same central notions of usefulness, redundancy, exhaustiveness, and counterexample witnesses, with extensions for Rust-specific patterns. (doc.rust-lang.org) A C++ pattern-matching proposal also cites the paper when discussing exhaustiveness and usefulness checking and identifies the algorithm as used by Rust. (isocpp.org) Thus, the paper’s principal lasting impact is its use as a foundation for practical exhaustiveness and redundancy diagnostics in modern pattern-matching compilers.