一句话：提出参数化子类型，一个可判定且严格推广刚性子类型的结构子类型片段，并给出饱和式判定过程与实现。
本文研究结构子类型与参数多态、递归定义类型构造子的交互。在这一场景下，结构子类型一般是不可判定的。作者为类型构造子引入参数性（parametricity）概念，并据此定义参数化子类型（parametric subtyping）：它概念简单、可判定、表达力强，且严格推广刚性子类型（rigid subtyping）。文章给出有效的基于饱和的判定过程，并证明其正确性；通过多种示例说明其适用性，同时将判定过程实现为可运行的 artifact。
We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this setting, we describe a notion of parametricity for type constructors and then exploit it to define parametric subtyping , a conceptually simple, decidable, and expressive fragment of structural subtyping that strictly generalizes rigid subtyping . We present and prove correct an effective saturation-based decision procedure for parametric subtyping, demonstrating its applicability using a variety of examples. We also provide an implementation of this decision procedure as an artifact.
@article{paperbot2658,
title = {Parametric Subtyping for Structural Parametric Polymorphism},
author = {Henry DeYoung and Andreia Mordido and Frank Pfenning and Ankush Das},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632932}
}