Structural subtyping and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider record as an argument to a function that expects a narrower one. However, the means by which they do so differs substantially, and the precise details of the relationship between them exists, at best, as folklore in literature. In this paper, we systematically study the relative expressive power of structural subtyping and parametric polymorphism. We focus our investigation on establishing the extent to which parametric polymorphism, in the form of row and presence polymorphism, can encode structural subtyping for variant and record types. We base our study on various Church-style $\lambda$-calculi extended with records and variants, different forms of structural subtyping, and row and presence polymorphism. We characterise expressiveness by exhibiting compositional translations between calculi. For each translation we prove a type preservation and operational correspondence result. We also prove a number of non-existence results. By imposing restrictions on both source and target types, we reveal further subtleties in the expressiveness landscape, the restrictions enabling otherwise impossible translations to be defined. More specifically, we prove that full subtyping cannot be encoded via polymorphism, but we show that several restricted forms of subtyping can be encoded via particular forms of polymorphism.
翻译:结构子类型化和参数多态为程序员提供了相似的灵活性和可重用性。例如,两种特性都允许程序员将更宽的记录作为参数传递给期望更窄记录的函数。然而,它们实现这一目标的方式存在显著差异,且二者之间关系的精确细节充其量仅作为学术界的传说存在。本文系统研究了结构子类型化与参数多态的相对表达能力。我们聚焦于探究以行多态和存在多态形式呈现的参数多态能在多大程度上编码变体类型和记录类型的结构子类型化。研究基于多种扩展了记录与变体的Church风格λ演算、不同形式的结构子类型化以及行多态与存在多态。通过展示演算之间的组合翻译来刻画表达能力,并为每种翻译证明类型保持性和操作对应性结果。我们还证明了若干不存在性结果。通过对源类型和目标类型施加限制,揭示了表达能力图景中更微妙的细节——这些限制使得原本不可能的翻译得以定义。具体而言,我们证明了完全子类型化无法通过多态编码,但展示了若干受限形式的子类型化可通过特定形式的多态进行编码。