嵌套类型和GADTs的参数化性
摘要：对嵌套数据类型的参数性及其产生的自由定理进行了研究。不采用System F的高等阶或依赖类型扩展来表示嵌套类型，而是采用函数式编程的观点，设计了一个Hindley-Milner风格的演算，其中包含了直接构建嵌套类型作为不动点的原语。我们的算法能够表示出现在文献中的所有嵌套类型，包括真正的嵌套类型。在项级别上，它支持原始模式匹配、映射函数和嵌套类型的折叠组合器。我们的主要贡献是构建了一个适用于我们的算法的参数模型。这既是精心设计又具有挑战性。特别是，为了确保解释嵌套类型的语义不动点的存在，并且为了建立一个适合我们的算法的合适的Identity Extension Lemma，我们的类型系统必须明确跟踪类型的函子性，并且将解释它们的函子的连续性条件适当地串联到模型构建过程中。我们还证明了我们的模型满足适当的抽象定理，并且在原始嵌套类型存在的情况下验证了参数性的所有标准结果。我们给出了几个具体的例子，说明我们的模型如何用于推导关于嵌套类型的有用的自由定理，包括一个短路径融合转换。最后，我们考虑将我们的结果推广到GADTs，并且认为在将左Kan扩展的函子解释为GADTs并且仍然保持参数性的方式中，我们对嵌套类型的参数模型的任何扩展都无法给出。
作者：Patricia Johann and Enrico Ghiorzi
论文ID：2101.04819
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22