Free Monads, Intrinsic Scoping, and Higher-Order Preunification
Nikolai Kudasov
TL;DR
The paper addresses the challenge of implementing higher-order unification in type checkers and proof assistants when dealing with dependent types or higher-order logics. It proposes a design based on second-order abstract syntax ($SOAS$), data types à la carte, and intrinsic scoping to generate a freely constructed object language from a signature, then derive a higher-order preunification procedure via a variant of $E$-unification. Key contributions include introducing free scoped monads, an extensible term-reduction framework, a backtracking preunification algorithm, and a demonstration of type checking and inference for Martin-Löf Type Theory (MLTT). This approach reduces the burden on language implementors by avoiding heavy $HOAS$ encodings while enabling modular, extensible type systems in proof assistants and similar tooling.
Abstract
Type checking algorithms and theorem provers rely on unification algorithms. In presence of type families or higher-order logic, higher-order (pre)unification (HOU) is required. Many HOU algorithms are expressed in terms of $λ$-calculus and require encodings, such as higher-order abstract syntax, which are sometimes not comfortable to work with for language implementors. To facilitate implementations of languages, proof assistants, and theorem provers, we propose a novel approach based on the second-order abstract syntax of Fiore, data types à la carte of Swierstra, and intrinsic scoping of Bird and Patterson. With our approach, an object language is generated freely from a given bifunctor. Then, given an evaluation function and making a few reasonable assumptions on it, we derive a higher-order preunification procedure on terms in the object language. More precisely, we apply a variant of $E$-unification for second-order syntax. Finally, we briefly demonstrate an application of this technique to implement type checking (with type inference) for Martin-Löf Type Theory, a dependent type theory.