渐进依赖类型编程的命题等同性
摘要：渐进性依赖类型对于逐步采用依赖类型代码提供了有原理的模糊类型和证明的语义，其中一些部分被省略。然而，目前的渐进依赖类型理论缺乏类型理论的一个核心特征：命题等号。Lennon-Bertrand等人表明，当自反证明$refl$是等号类型的唯一闭值时，扩展的CIC与命题等式违反了静态观察等价性。在运行时，外延相等的函数应该无法区分，但等号和类型不确定性的组合允许区分外延相等但句法上不同的函数的上下文。本文介绍了一种支持命题等式的逐渐类型化语言。我们通过设计一个等号类型来避免上述问题，其中$refl$不是唯一的闭合成员。相反，每个等号证明都携带着至少与等式术语一样精确的术语，作为它们可能相等的证明。这些证明在程序运行时跟踪部分类型信息，当该信息表明两个等式术语无疑不一致时，引发错误。类型信息的组合被内置为语言的构造，对于变量阻塞了函数体的求值，因此推迟了组合。通过推迟，我们确保扩展相等的函数组合时没有错误，从而防止上下文进行区分。我们描述了为该系统设计一致性和精确性关系的挑战，以及对这些挑战的解决方案。最后，我们证明了重要的元理论：类型安全性，CIC的保守嵌入，正则性以及Siek等人的渐进性保证。
作者：Joseph Eremondi, Ronald Garcia, ''Eric Tanter
论文ID：2205.01241
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-05-04