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 online.

翻译：我们研究了结构子类型与参数多态及递归定义的类型构造器之间的交互作用。尽管在此设定下结构子类型不可判定，但我们提出了类型构造器的参数性概念，并利用该概念定义了参量子类型——它是结构子类型的一个概念简洁、可判定且富有表现力的片段，严格推广了刚性子类型。我们提出并证明了基于饱和的参量子类型有效判定过程，通过多种实例展示了其适用性，同时在线提供了该判定过程的实现。