嵌套类型与GADT的参数性
Parametricity for Nested Types and GADTs
AI总结：
本文为嵌套数据类型设计了一个Hindley-Milner风格演算，并构建了其参数模型，证明了抽象定理，可用于推导自由定理，同时论证了该模型无法扩展到GADT。
摘要：
本文考虑了嵌套数据类型及其由此产生的自由定理的参数性。我们没有通过System F的高阶类型或依赖类型扩展中的Church编码来表示嵌套类型，而是采用函数式编程的视角，设计了一个Hindley-Milner风格的演算，其中包含直接将嵌套类型构造为不动点的原语。我们的演算可以表达文献中出现的所有嵌套类型，包括真正的嵌套类型。在项层面，它支持嵌套类型的基本模式匹配、映射函数和折叠组合子。我们的主要贡献是为我们的演算构建了一个参数模型。这既微妙又具有挑战性。特别是，为了确保解释嵌套类型的语义不动点的存在性，从而为我们的演算建立合适的恒等扩展引理，我们的类型系统必须显式跟踪类型的函子性，并且解释它们的函子上的余连续性条件必须适当地贯穿模型构建。我们还证明了我们的模型满足适当的抽象定理，并验证了在存在基本嵌套类型的情况下参数性的所有标准推论。我们给出了几个具体示例，说明如何使用我们的模型来推导有用的自由定理，包括针对嵌套类型程序的短路融合变换。最后，我们考虑了将我们的结果推广到GADT，并论证了我们对嵌套类型的参数模型的任何扩展都不能给出GADT在左Kan扩展意义上的函子解释，同时仍然保持参数性。
英文摘要：
This paper considers parametricity and its consequent free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints. Our calculus can express all nested types appearing in the literature, including truly nested types. At the level of terms, it supports primitive pattern matching, map functions, and fold combinators for nested types. Our main contribution is the construction of a parametric model for our calculus. This is both delicate and challenging. In particular, to ensure the existence of semantic fixpoints interpreting nested types, and thus to establish a suitable Identity Extension Lemma for our calculus, our type system must explicitly track functoriality of types, and cocontinuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We also prove that our model satisfies an appropriate Abstraction Theorem, as well as that it verifies all standard consequences of parametricity in the presence of primitive nested types. We give several concrete examples illustrating how our model can be used to derive useful free theorems, including a short cut fusion transformation, for programs over nested types. Finally, we consider generalizing our results to GADTs, and argue that no extension of our parametric model for nested types can give a functorial interpretation of GADTs in terms of left Kan extensions and still be parametric.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
