Coverage Semantics for Dependent Pattern Matching
Joseph Eremondi, Ohad Kammar
cs.PL
Jan 30, 2025 · v1
TL;DR
The sufficient criterion for sound coverages and the key sheaf-theoretic properties are mechanized in Lean 4, with an archived Zenodo artifact.
Abstract
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.
Problem
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.
Approach
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.
Results
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.