一句话：提出结合行类型/行多态与类型类特设多态的可扩展数据类型语言设计，并给出机器化验证的可靠性证明。
论文研究如何在统一语言中同时支持可扩展数据类型与特设多态。传统行类型与行多态擅长表达可扩展记录/变体，而类型类提供 ad-hoc 多态，但二者结合缺乏清晰的形式化。作者提出新语言设计，引入若干面向行上泛型操作的新构造与约束，并将其形式化为源演算 λρ⇒，该演算可精化为目标演算 Fω⊗⊕。作者证明目标演算类型安全，且精化过程可靠，从而建立源演算的可靠性；所有证明均在 Lean 4 中机器化。最后使用 Brown Benchmark for Table Types 评估类型系统，表明可扩展行与类型类对表类型具有实用性。
This paper proposes a novel language design that combines extensible data types, implemented through row types and row polymorphism, with ad-hoc polymorphism, implemented through type classes. Our design introduces several new constructs and constraints useful for generic operations over rows. We formalize our design in a source calculus λ ρ ⇒ , which elaborates into a target calculus F ω ⊗⊕ . We prove that the target calculus is type-safe and that the elaboration is sound, thus establishing the soundness of λ ρ ⇒ . All proofs are mechanized in the Lean 4 proof assistant. Furthermore, we evaluate our type system using the Brown Benchmark for Table Types, demonstrating the utility of extensible rows with type classes for table types.
@article{TooheyCJX26,
title = {Extensible Data Types with Ad-Hoc Polymorphism},
author = {Matthew Toohey and Yanning Chen and Ara Jamalzadeh and Ningning Xie},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776662}
}