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{paperbot3942,
  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}
}