一句话：提出在记录类型构造子内直接支持行变量布尔组合，使集合论类型获得行多态，并实现于 SSTT 与 MLsem。
集合论类型通过并、交、补支持表达力强的记录类型，但缺少行多态，难以类型化在记录间传播未知字段的操作。已有工作允许类型替换中出现行的布尔组合，导致形式化复杂且 tallying 算法不完备。本文改为在记录类型构造子内直接允许行变量的布尔组合，并令记录尾与任意字段同形。如此行变量仍映射到单个行，子类型与 tallying 算法自然扩展；tallying 对在约束未提及标签上恒定的所有解完备。作者在 SSTT 库和 MLsem 类型检查器中实现，首次结合语义子类型与行多态，并通过编码 R 的异构列表、可变参数函数和类分派展示表达力。
Set-theoretic types support expressive record types through unions, intersections, and negations, but they lack the row polymorphism needed to type operations that propagate unknown fields across records. Prior work addresses this by allowing Boolean combinations of rows in type substitutions, which complicates the formalism and prevents the tallying algorithm from being complete. We propose an alternative: instead of enriching substitutions, we allow Boolean combinations of row variables directly within record type constructors, where the tail of a record has the same shape as any field. This design keeps substitutions simple---a row variable maps to a single row---and yields a natural extension of the subtyping and tallying algorithms. Tallying is complete for all solutions whose rows are constant over labels not mentioned in the constraints. We implement our approach in the set-theoretic type library SSTT and the type checker MLsem, providing the first implementation of a type system that combines semantic subtyping with row polymorphism. We demonstrate the expressiveness of the system by encoding several data structures from the R programming language: heterogeneous lists, variadic function arguments, and class-based dispatch.
@article{paperbot12136,
title = {Revisiting Row Polymorphism for Set-Theoretic Types},
author = {Mickaël Laurent and Pierre Donat-Bouillud and Filip Křikava and Jan Vitek},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839505}
}