Implementing Dependent Type Theory Inhabitation and Unification

TL;DR

This paper presents Canonical-min, a compact, sound, and complete solver for inhabitation and unification in dependent type theory, along with a new benchmark for evaluating such solvers.

Contribution

It introduces Canonical-min, a novel, efficient solver for inhabitation and unification in dependent type theory, implemented in Lean, and presents DTTBench for benchmarking.

Findings

Canonical-min is sound and complete for inhabitation and unification.

The solver is implemented in only 185 lines of Lean code.

DTTBench provides a new standard for evaluating dependent type theory solvers.

Abstract

Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synthesis. We introduce Canonical-min, a sound and complete solver for inhabitation and unification in dependent type theory, implemented in 185 lines of Lean code. This paper describes a novel implementation of dependent type theory and a monadic framework to transform the type checker into a performant solver. Finally, we introduce DTTBench, a benchmark for type inhabitation in dependent type theory.