一句话：提出用行类型统一支持可扩展记录/变体上的泛型编程，并在 System Rω 中形式化与给出指称语义。
本文研究如何对可扩展数据类型进行泛型编程。作者以行类型刻画记录与变体的结构，用其表达记录/变体子类型、记录扩展以及 case 分支的模块化组合；进一步把行类型推广到对行本身的泛型操作，支持从字段类型提升操作到记录和变体，并刻画变体 case 块与带标签函数记录之间的对偶，而不对字段或构造器作特殊要求。方法上提出 System Rω——Fω 加行类型的扩展，并为其分层版本给出 Agda 中的指称语义。该工作为可扩展记录/变体提供更少 ad hoc 的泛型编程机制，并通过语义模型奠定理论基础。
We present a novel approach to generic programming over extensible data types. Row types capture the structure of records and variants, and can be used to express record and variant subtyping, record extension, and modular composition of case branches. We extend row typing to capture generic programming over rows themselves, capturing patterns including lifting operations to records and variations from their component types, and the duality between cases blocks over variants and records of labeled functions, without placing specific requirements on the fields or constructors present in the records and variants. We formalize our approach in System R𝜔, an extension of F𝜔 with row types, and give a denotational semantics for (stratified) R𝜔 in Agda.
@article{paperbot1920,
title = {Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc},
author = {Alex Hubers and J. Garrett Morris},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607843}
}