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.

翻译：类型检查算法和定理证明器依赖于合一算法。在存在类型族或高阶逻辑的情况下，需要高阶（预）合一（HOU）。许多HOU算法以λ-演算的形式表达，并需要诸如高阶抽象语法之类的编码，这对语言实现者而言有时不便使用。为了促进语言、证明助手和定理证明器的实现，我们提出了一种基于Fiore的二阶抽象语法、Swierstra的“组合数据类型”（data types à la carte）以及Bird和Patterson的内在作用域的新方法。通过我们的方法，目标语言从一个给定的双函子自由生成。然后，给定一个求值函数并对其做出若干合理假设，我们推导出目标语言项上的高阶预合一过程。更精确地说，我们应用了一种用于二阶语法的E-合一变体。最后，我们简要展示了该技术在实现马丁-洛夫类型论（一种依赖类型论）的类型检查（含类型推断）中的应用。