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.
翻译:本文审视了嵌入数据类型的近似度及其随后的免费理论。 我们不是在系统F的更高类型或依附型扩展中通过教会编码代表嵌入类型。 我们采取功能性编程视角, 并设计了Hindley- Milner风格的计算器, 以原始方式直接建造嵌入类型作为固定点。 我们的计算仪可以明确显示文献中出现的所有嵌入类型, 包括真正的嵌入类型。 在术语层面, 它支持原始模式匹配、 地图功能和嵌入类型折叠组合。 我们的主要贡献是构建一个我们计算系统精度更高或依附型扩展的参数模型。 这既微妙又具有挑战性。 特别是为了确保存在能解释嵌入型类型的精度固定点, 从而为我们的缩入类型建立合适的身份扩展器。 我们的计算系统必须明确跟踪各种类型, 包括真正嵌入型类型, 以及解释这些类型时的缩略图的缩略图条件, 在整个建模中, 仍然可以适当地排列。 我们还证明我们的模型能够满足一个适当的缩缩缩缩缩模型, 将模型的缩缩图, 用来解释结果, 用来解释。