← All papers
First page of Coverage Semantics for Dependent Pattern Matching

Coverage Semantics for Dependent Pattern Matching

Joseph Eremondi, Ohad Kammar

cs.PL Jan 30, 2025 · v1
The sufficient criterion for sound coverages and the key sheaf-theoretic properties are mechanized in Lean 4, with an archived Zenodo artifact.
Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching as primitive, theoretical presentations give semantics to pattern matching by elaborating to eliminators. Though theoretically convenient, eliminators can be awkward and verbose, particularly for complex combinations of patterns. This work aims to bridge the theory-practice gap by presenting a direct categorical semantics for pattern matching, which does not elaborate to eliminators. This is achieved using sheaf theory to describe when sets of arrows (terms) can be amalgamated into a single arrow. We present a language with top-level dependent pattern matching, without specifying which sets of patterns are considered covering for a match. Then, we give a sufficient criterion for which pattern-sets admit a sound model: patterns should be in the canonical coverage for the category of contexts. Finally, we use sheaf-theoretic saturation conditions to devise some allowable sets of patterns. We are able to express and exceed the status quo, giving semantics for datatype constructors, nested patterns, absurd patterns, propositional equality, and dot patterns.

Proof assistants implement dependent pattern matching as a primitive. Theoretical treatments instead give it semantics by elaborating to eliminators, which is awkward for complex combinations of patterns. The authors want a direct categorical semantics for pattern matching that avoids this elaboration.

The authors define CoverTT, a Martin-Löf-style type theory parameterized by a coverage that specifies which sets of patterns may be matched. They interpret it in categories with families. Sheaf theory determines when a set of arrows (terms) can be amalgamated into a single arrow. The sufficient criterion and key properties are mechanized in Lean 4.

Patterns lying in the canonical coverage of the category of contexts admit a sound model. Saturation conditions yield covers for constructors, nested patterns, absurd patterns, propositional equality and dot patterns, demonstrated on foldr1. Mechanizing full model soundness and the coverage-building rules is ongoing.