一句话：在带递归类型和内部化类型等式的 System Fω 扩展中直接编码 GADTs，并给出类型可靠性与关系模型。
本文研究广义代数数据类型（GADTs）在一个极简 λ 演算中的直接编码。作者将 System Fω 扩展为带递归类型、内部化类型等式以及单射常量类型构造子的系统，并展示 GADTs 及相应模式匹配可直接在该演算中表达，从而把它视为理想化的现代函数式语言。文章证明内部化类型等式与单射规则通过一个在 Fω 中的非宏可表达性结果提升了表达能力，并以语法论证证明类型可靠。作者还构造了两类关系模型：简单的 unary 模型展示处理等式约束所需的新颖两阶段解释技术；更精细的 binary 模型则首次支持在配备 GADTs 的演算中对数据抽象进行形式推理。
This paper considers direct encodings of generalized algebraic data types (GADTs) in a minimal suitable lambda-calculus. To this end, we develop an extension of System F ω with recursive types and internalized type equalities with injective constant type constructors. We show how GADTs and associated pattern-matching constructs can be directly expressed in the calculus, thus showing that it may be treated as a highly idealized modern functional programming language. We prove that the internalized type equalities in conjunction with injectivity rules increase the expressive power of the calculus by establishing a non-macro-expressibility result in F ω , and prove the system type-sound via a syntactic argument. Finally, we build two relational models of our calculus: a simple, unary model that illustrates a novel, two-stage interpretation technique, necessary to account for the equational constraints; and a more sophisticated, binary model that relaxes the construction to allow, for the first time, formal reasoning about data-abstraction in a calculus equipped with GADTs.
@article{paperbot2583,
title = {The Essence of Generalized Algebraic Data Types},
author = {Filip Sieczkowski and Sergei Stepanenko and Jonathan Sterling and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632866}
}