代数数据类型

形式陈述 ​

一个代数数据类型可由有限个构造子描述为

$$D(\overline{A})\cong \sum _{i=1}^k{C}_i(\prod _{j=1}^{n_i}{T}_{ij}(\overline{A},D)).$$

外层和类型公理库和类型Sum type · Variant type其值从若干带标签分支中选择一个的类型。表示值从 $C_1,\dots ,C_k$ 中选择一个构造子；该分支内部的积类型公理库积类型Product type其值由两个分量组成并支持投影的类型。同时携带 $n_i$ 个字段。零字段构造子的负载是单位类型 $1$。若字段类型再次引用 $D$，定义还使用递归类型公理库递归类型Recursive type通过类型方程把类型变量递归绑定到包含自身的类型。；不含递归引用的枚举和记录式变体仍然是代数数据类型。

例如

$$\mathrm{Option}(A)\cong 1+A,\mathrm{List}(A)\cong \mu X.1+A\times X,$$

分别对应 None | Some A 与 Nil | Cons(A, List A)。构造器是和类型的注入再配合字段元组；模式匹配是相应的消去形式：它先依据构造子选择分支，再把该分支携带的字段绑定给分支体。模式匹配是否穷尽、是否有不可达分支，是建立在类型定义之上的静态检查问题，不是构造子声明本身。

“参数化”“递归”“代数”描述不同维度。Option A 对类型参数 $A$ 抽象但不递归，非参数化的树也可以递归；代数数据类型把这些机制与有限和、积组合起来。这里必须写出全称，避免与“抽象数据类型”（abstract data type）共享缩写 ADT 时产生概念混淆。

直觉 ​

读取一个代数数据类型可以先问两个问题：当前值是哪一种情况，每种情况又带着哪些材料。构造子的集合回答前一个问题，字段列表回答后一个问题。类型声明因此像一张封闭的结构图，而不是一串互不相关的类名；程序消费值时必须沿这张图逐个处理可能分支。

所谓“代数”来自类型构造的形状运算。和对应选择，积对应组合，递归让同一形状继续出现在下一层。这个视角解释了为什么编译器常把值实现为“标签加负载”，也解释了模式匹配为何能同时恢复分支身份与字段类型。

例子与边界 ​

二叉树可定义为 Empty | Node A (Tree A) (Tree A)，对应方程

$$\mathrm{Tree}(A)\cong 1+A\times \mathrm{Tree}(A)\times \mathrm{Tree}(A).$$

Empty 选择单位分支，Node 选择带三个字段的分支。求节点数时，Empty 返回零，Node 分支递归处理两棵子树；不同分支的字段数和字段类型由构造器决定，不能在 Empty 分支读取不存在的元素。

并非任何可在语言中声明的类型都因此成为代数数据类型。函数类型表达从输入到输出的行为，存在类型隐藏某个表示，带私有状态的对象通过接口封装操作；它们不能仅因语法上有一个类型名就还原成有限构造子的和。广义代数数据类型还允许构造器返回带特定索引的结果类型，例如某构造器只生成 Expr Int；这需要等式约束与索引精化，超出了本页的普通参数化定义。

递归方程也不自动带来良基性。一个允许无限展开或负位置递归的类型可以是递归类型，却不一定是由有限构造步骤生成的归纳类型公理库归纳类型Inductive type · Inductive datatype由有限构造步骤生成的最小递归数据类型，并以严格正性保障其递归结构良好。。因此不能从“写成和与积的递归方程”直接推出结构归纳或终止的 fold。

推论与应用 ​

代数数据类型把数据定义与按形状分支的程序组织在一起。编译器可据构造子集合检查模式覆盖，按标签布局运行时表示，并利用单构造子或无负载分支做表示优化；这些算法化工作必须保持声明式构造与消去规则的含义。

在函数式程序设计中，语法树、配置状态、协议消息和错误结果都常用代数数据类型建模。它们也为结构递归提供清晰的输入形状，但只有进一步满足严格正性和良基生成条件时，才获得归纳类型所保证的递归与证明原则。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，variants, products, and recursive types。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，sum, product, recursive, and inductive types。
• Luca Cardelli and Peter Wegner, “On Understanding Types, Data Abstraction, and Polymorphism,” ACM Computing Surveys 17(4), 1985，type constructors and data abstraction terminology。