论文标题
免费的单子，内在范围和高阶预校准
Free Monads, Intrinsic Scoping, and Higher-Order Preunification
论文作者
论文摘要
类型检查算法和定理侵略依赖于统一算法。在存在类型的家族或高阶逻辑的情况下，需要高阶（PER）统一（HOU）。许多HOU算法以$λ$ -calculus表示，需要编码，例如高阶抽象语法，有时与语言实施者一起使用它们不舒服。为了促进语言，证明助手和定理掠夺的实施，我们提出了一种基于fiore的二阶抽象语法，数据类型的新方法，swiersstra的数据类型以及鸟类和帕特森的内在范围。通过我们的方法，对象语言是由给定的双交径自由生成的。然后，给定评估功能并在其上做出一些合理的假设，我们在对象语言中根据术语得出了一个高阶的预校准程序。更确切地说，我们在二阶语法上应用$ e $ $ $ unifate的变体。最后，我们简要地证明了该技术在Martin-Löf类型理论（一种依赖类型理论）中实施类型检查（具有类型推理）的应用。
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.
