一句话：系统比较结构子类型与参数多态的表达力，证明完整子类型无法由多态编码，但若干受限子类型可以。
结构子类型与参数多态都能为程序员提供灵活性与可复用性，例如把更宽的记录传给期望更窄记录的函数；但二者实现方式不同，其精确关系此前多为民间知识。本文系统研究二者的相对表达力：以多种扩展记录与变体的 Church 风格 λ-演算为基础，考虑不同形式的结构子类型以及行多态和 presence 多态。作者通过给出演算间的组合式翻译来刻画表达力，并对每个翻译证明类型保持与操作对应。论文还证明若干不存在性结果：完整子类型不能通过多态编码，但若干受限形式的子类型可由特定形式的多态编码；对源与目标类型施加限制会揭示更细微的表达力图景。
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 λ-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.
@article{paperbot1826,
title = {Structural Subtyping as Parametric Polymorphism},
author = {Wenhao Tang and Daniel Hillerström and James McKinna and Michel Steuwer and Ornela Dardha and Rongxiao Fu and Sam Lindley},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622836}
}