一句话：提出支持命题相等性的渐进依赖类型语言，引入等式见证以保持外延相等函数不可区分，并证明类型安全与渐进保证。
渐进依赖类型支持不精确类型与证明的逐步采用，但现有理论缺少命题相等性。已有工作指出，若 refl 是相等类型唯一闭值，则 CIC 的渐进扩展会破坏静态观察等价，使外延相等函数在运行时被区分。本文提出一种支持命题相等性的渐进依赖类型语言：每个相等证明附带一个至少与等式两边一样精确的项作为见证，记录部分类型信息；当信息显示两项确实不一致时报错。类型信息的复合被内化为语言构造，并对因变量阻塞的函数体推迟计算，从而保证外延相等函数可复合且不可区分。文章给出一致性、精度关系及元理论证明，包括类型安全、CIC 保守嵌入、弱典范性和 Siek 等人的渐进保证。
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have been omitted. Current theories of gradual dependent types, though, lack a central feature of type theory: propositional equality. Lennon-Bertrand et al. show that, when the reflexive proof refl is the only closed value of an equality type, a gradual extension of the Calculus of Inductive Constructions (CIC) with propositional equality violates static observational equivalences. Extensionally-equal functions should be indistinguishable at run time, but they can be distinguished using a combination of equality and type imprecision. This work presents a gradual dependently typed language that supports propositional equality. We avoid the above issues by devising an equality type of which refl is not the only closed inhabitant. Instead, each equality proof is accompanied by a term that is at least as precise as the equated terms, acting as a witness of their plausible equality. These witnesses track partial type information as a program runs, raising errors when that information shows that two equated terms are undeniably inconsistent. Composition of type information is internalized as a construct of the language, and is deferred for function bodies whose evaluation is blocked by variables. We thus ensure that extensionally-equal functions compose without error, thereby preventing contexts from distinguishing them. We describe the challenges of designing consistency and precision relations for this system, along with solutions to these challenges. Finally, we prove important metatheory: type safety, conservative embedding of CIC, weak canonicity, and the gradual guarantees of Siek et al., which ensure that reducing a program’s precision introduces no new static or dynamic errors.
@article{paperbot1498,
title = {Propositional equality for gradual dependently typed programming},
author = {Joseph Eremondi and Ronald Garcia and Éric Tanter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547627}
}