Structural subtyping and parametric polymorphism provide a similar kind of flexibility and reusability to programmers. For example, both enable the programmer to supply 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.
翻译:结构子类型和参数化多态都为程序员提供了类似的灵活性和可重用性。例如,两者都使程序员能够将更宽的记录作为参数传递给期望更窄的记录的函数。然而,它们实现的方式存在很大差异,并且它们之间的关系的确切细节在文献中至多是民间故事。在本文中,我们系统地研究了结构子类型和参数化多态的相对表达能力。我们的关注点在于建立参数化多态(以行和存在多态的形式)可以为变量和记录类型编码结构子类型的程度。我们基于包含记录和变量的不同形式的结构子类型和行和存在多态的各种 Church 风格 $\lambda$-演算研究了这个问题。我们通过展示演算之间的组合翻译来表征表达能力。针对每个翻译,我们证明了类型保持和操作对应结果。我们还证明了一些不存在的结果。通过对源类型和目标类型施加限制,我们揭示了表达能力领域中的进一步细微差别,这些限制使得原本不可能的翻译得以定义。