一句话：提出三层 RETT，在完全依赖类型论中首次一致地推理异常项，并提供 Coq 插件 CoqRETT。
在证明助手的类型论中，异常长期缺失；传统补偿方案在编程与推理上均有严重缺陷。Pédrot 与 Tabareau 的异常 CIC 扩展虽保持依赖消除、可判定类型检查与典范性，但作为逻辑系统不一致；用参数性强制异常局部捕获虽恢复一致性，却无法推理异常程序与部分函数。本文提出合理异常类型论 RETT，以三层结构调和该两难：异常层允许项抛出异常，中介层要求异常项可证参数性，纯层指称非异常项但可引用异常项；三层分别由可预测宇宙层级实现。作者在 Coq 中实例化 RETT：非纯（异常）层对应可预测宇宙层级，纯层用非可预测命题宇宙，中介层通过参数性类型类具体化，并给出 CoqRETT 插件。RETT 是首个支持对异常项进行一致推理的完整依赖类型论。
Traditional approaches to compensate for the lack of exceptions in type theories for proof assistants have severe drawbacks from both a programming and a reasoning perspective. Pédrot and Tabareau recently extended the Calculus of Inductive Constructions (CIC) with exceptions. The new exceptional type theory is interpreted by a translation into CIC, covering full dependent elimination, decidable type-checking and canonicity. However, the exceptional theory is inconsistent as a logical system. To recover consistency, Pédrot and Tabareau propose an additional translation that uses parametricity to enforce that all exceptions are caught locally. While this enforcement brings logical expressivity gains over CIC, it completely prevents reasoning about exceptional programs such as partial functions. This work addresses the dilemma between exceptions and consistency in a more flexible manner, with the Reasonably Exceptional Type Theory (RETT). RETT is structured in three layers: (a) the exceptional layer, in which all terms can raise exceptions; (b) the mediation layer, in which exceptional terms must be provably parametric; (c) the pure layer, in which terms are non-exceptional, but can refer to exceptional terms. We present the general theory of RETT, where each layer is realized by a predicative hierarchy of universes, and develop an instance of RETT in Coq: the impure layer corresponds to the predicative universe hierarchy, the pure layer is realized by the impredicative universe of propositions, and the mediation layer is reified via a parametricity type class. RETT is the first full dependent type theory to support consistent reasoning about exceptional terms, and the CoqRETT plugin readily brings this ability to Coq programmers.
@article{paperbot612,
title = {A reasonably exceptional type theory},
author = {Pierre-Marie Pédrot and Nicolas Tabareau and Hans Jacob Fehrmann and Éric Tanter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341712}
}