Free Monads, Intrinsic Scoping, and Higher-Order Preunification

TL;DR

This paper introduces a new approach for higher-order preunification using second-order abstract syntax and intrinsic scoping, simplifying implementation in language tools and theorem provers.

Contribution

It presents a novel method combining second-order syntax, intrinsic scoping, and free data type generation to facilitate higher-order unification in practical language implementations.

Findings

Develops a higher-order preunification procedure based on E-unification.

Applies the method to type checking in Martin-Löf Type Theory.

Simplifies implementation of higher-order unification algorithms.

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 $\lambda$-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 \`a 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\"of Type Theory, a dependent type theory.