Dependent pattern matching: theory and implementation

Jesper Cockx

Programming is hard. This is proven again and again by the numerous bugs, vulnerabilities, and other weird behaviours in the software we use every day. Dependently typed programming languages such as Agda allow the programmer to avoid many of these problems by encoding properties of programs in their types and statically checking that they hold. Compared to other tools for program verification, dependently typed languages are unique because they can be used both as a programming language and as an interactive proof assistant. In particular, the same techniques used for writing programs can also be used for writing proofs about these programs. Dependent pattern matching (Coquand, 1992) is one such technique for writing programs and proofs in dependently typed languages. It combines the intuitive notation of pattern matching from functional languages such as Haskell and ML with the mathematical techniques of case analysis and induction. Dependent pattern matching relies on a unification algorithm to specialize the type of each equation and automatically rule out impossible cases. Thanks to this unification algorithm, definitions by dependent pattern matching are often much shorter and easier to read compared to those written using other more primitive techniques. However, the original formulation of dependent pattern matching by Coquand is incompatible with new versions of dependent type theory such as homotopy type theory (HoTT). The source of this incompatibility lies in the unification algorithm employed for case splitting, which implicitly relies on two axioms – uniqueness of identity proofs and injectivity of type constructors – that are not permissible in HoTT. I present a new proof-relevant framework for reasoning formally about unification in a dependently typed setting. In this framework, each unification rule not only simplifies the equations but also produces evidence of its correctness. This evidence guarantees that all unification rules are correct by construction without relying on any axioms, and also gives a computational characterization to each unification rule. Based on these ideas, I implemented a complete overhaul of the algorithm for checking definitions by dependent pattern matching in Agda. My new implementation fixes a substantial number of issues in the previous version, and is at the same time more permissive than the old ad-hoc restrictions. Thus it puts the whole system back on a strong foundation. In addition, my work has already been used as the basis for other implementations of dependent pattern matching, such as the Equations package for Coq and the Lean theorem prover.

References. Thierry Coquand (1992). Pattern matching with dependent types. TYPES ’92. Jesper Cockx (2017). Dependent pattern matching and proof-relevant unification. PhD thesis.

---

Previous: Albert ten Napel | A type system for dynamic instances
Next: Jorge A. Pérez | Session Types and Higher-Order Concurrency