一句话：提出 GRIP，一个扩展 CastCIC、内蕴精度和异常处理的渐进类型论，兼顾规范化与 CIC 保守扩张。
将 CIC 渐进化需权衡规范化、渐进性和相对 CIC 的保守性，已有 GCIC 只能牺牲其一。面向渐进证明助手，还需处理 error/unknown 通配项导致任意定理可证、一般索引归纳族与相等类型、归约中的类型不匹配，以及精度和渐进性仅外蕴等问题。本文提出 CastCIC 的扩展 GRIP，引入内蕴精度和一般异常处理，并通过按宇宙层级解释 unknown，使 GRIP 对一大类项满足渐进性，保持规范化且保守扩展 CIC；内蕴精度支持系统内渐进推理和 gradual subset types。作者在 Coq 中形式化模型，并提供 Agda 原型。
Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently, GCIC has been proposed as a parametrized gradual type theory that admits three variants, each sacrificing one of these properties. For devising a gradual proof assistant based on CIC, normalization and conservativity with respect to CIC are key, but the tension with graduality needs to be addressed. Additionally, several challenges remain: (1) The presence of two wildcard terms at any type---the error and unknown terms---enables trivial proofs of any theorem, jeopardizing the use of a gradual type theory in a proof assistant; (2) Supporting general indexed inductive families, most prominently equality, is an open problem; (3) Theoretical accounts of gradual typing and graduality so far do not support handling type mismatches detected during reduction; (4) Precision and graduality are external notions not amenable to reasoning within a gradual type theory. All these issues manifest primally in CastCIC, the cast calculus used to define GCIC. In this work, we present an extension of CastCIC called GRIP. GRIP is a reasonably gradual type theory that addresses the issues above, featuring internal precision and general exception handling. By adopting a novel interpretation of the unknown term that carefully accounts for universe levels, GRIP satisfies graduality for a large and well-defined class of terms, in addition to being normalizing and a conservative extension of CIC. Internal precision supports reasoning about graduality within GRIP itself, for instance to characterize gradual exception-handling terms, and supports gradual subset types. We develop the metatheory of GRIP using a model formalized in Coq, and provide a prototype implementation of GRIP in Agda.
@article{paperbot1499,
title = {A reasonably gradual type theory},
author = {Kenji Maillard and Meven Lennon-Bertrand and Nicolas Tabareau and Éric Tanter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547655}
}