Coverage Semantics for Dependent Pattern Matching

TL;DR

This paper introduces a direct categorical semantics for dependent pattern matching using sheaf theory, bridging the gap between practical implementations and theoretical foundations without relying on eliminators.

Contribution

It presents a novel sheaf-theoretic approach to semantics for dependent pattern matching, enabling a more direct and expressive understanding of pattern matching in dependently typed languages.

Findings

Provides a sound model for top-level dependent pattern matching

Expresses semantics for complex pattern types like nested and absurd patterns

Surpasses existing semantics by including datatype constructors and propositional equality

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.