一句话：提出 row theories 与 qualified types，统一抽象可扩展记录和变体，并保持 coherence 与主类型。
现有可扩展数据类型系统以行类型和行多态为核心，但缺少对记录拼接/投影与变体注入/分支的统一抽象。本文提出一种新的类型化语言，引入 row theories，即行类型的 monoidal 泛化，为这些操作提供一般解释；并通过 qualified types 将记录和变体的语义抽象到不同 row theories 上。类型限定符的证据具有计算内容，决定记录与变体操作的实现。作者给出从该演算到多态 λ-演算的模块化翻译，并可在多种 row theories 下实例化。结果表明，该方法能为其他系统无法类型化的项赋予类型，同时保持 coherence、principal types 等强元理论性质，并支持模块化组合解释器。
We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism. Extensible data types are a powerful addition to traditional functional programming languages, capturing ideas from OOP-like record extension and polymorphism to modular compositional interpreters. We introduce row theories, a monoidal generalization of row types, giving a general account of record concatenation and projection (dually, variant injection and branching). We realize them via qualified types, abstracting the interpretation of records and variants over different row theories. Our approach naturally types terms untypable in other systems of extensible data types, while maintaining strong metatheoretic properties, such as coherence and principal types. Evidence for type qualifiers has computational content, determining the implementation of record and variant operations; we demonstrate this in giving a modular translation from our calculus, instantiated with various row theories, to polymorphic λ-calculus.
@article{paperbot653,
title = {Abstracting extensible data types: or, rows by any other name},
author = {J. Garrett Morris and James McKinna},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290325}
}