一句话：提出证明相关的合一框架，使合一规则只依赖所在类型论自身的公理，并据此重写 Agda 的合一算法修复大量缺陷。
Agda、Coq、Idris 等依赖类型语言用一阶语法合一来检查依赖模式匹配定义，但标准合一算法隐含依赖同一性证明唯一性（UIP）、类型构造子单射等原则；这些原则在同伦类型论等新兴类型论中不可接受，导致程序与证明无法使用依赖模式匹配，难以编写和维护。本文提出一个用于形式化推理依赖类型设定下合一的 proof-relevant 框架：合一规则不仅计算 unifier，还计算相应的可靠性证明，即两组方程之间的等价。以证明相关的方式重写标准规则可保证理论可靠性不被破坏，并允许安全地加入利用类型依赖的新规则，如记录类型的 eta-等式规则，以及求解等式证明之间方程的高维合一规则。作者用该框架彻底重写 Agda 的合一算法，以形式验证的规则取代先前的 ad-hoc 限制，修复了大量 bug，并为将来整合高阶归纳类型等新原则奠定基础。
Abstract Dependently typed languages such as Agda, Coq, and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, standard unification algorithms implicitly rely on principles such as uniqueness of identity proofs and injectivity of type constructors . These principles are inadmissible in many type theories, particularly in the new and promising branch known as homotopy type theory. As a result, programs and proofs in these new theories cannot make use of dependent pattern matching or other techniques relying on unification, and are as a result much harder to write, modify, and understand. This paper proposes a proof-relevant framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding soundness proof in the form of an equivalence between two sets of equations. By rephrasing the standard unification rules in a proof-relevant manner, they are guaranteed to preserve soundness of the theory. In addition, it enables us to safely add new rules that can exploit the dependencies between the types of equations, such as rules for eta-equality of record types and higher dimensional unification rules for solving equations between equality proofs. Using our framework, we implemented a complete overhaul of the unification algorithm used by Agda. As a result, we were able to replace previous ad-hoc restrictions with formally verified unification rules, fixing a substantial number of bugs in the process. In the future, we may also want to integrate new principles with pattern matching, for example, the higher inductive types introduced by homotopy type theory. Our framework also provides a solid basis for such extensions to be built on.
@article{paperbot333,
title = {Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory},
author = {JESPER COCKX and DOMINIQUE DEVRIESE},
journal = {Journal of Functional Programming},
volume = {28},
year = {2018},
doi = {10.1017/s095679681800014x}
}