最近被问到了关于ADT的事情呢，于是想写一篇速通关于ADT、递归类型是怎么回事.
啥是ADT呢
代数数据类型（Algebraic Data Types）顾名思义就是可以做运算的数据类型. 这里算的数字很简单就是这个数据类型的值的数量.
- 1：只有一个值的类型，在Haskell中记作
()，它有很多名字Unit、top $\top$、或者就叫$1$. - 加法：对应和类型（sum types）. 类型
A和类型B的值都是和类型A + B的值，不过我们要指定这个值是来自A还是B. - 2：众所周知，$2 = 1+1$. 我们把两个1加起来
data Two = L () | R ()，就得到了有两个值的类型。对了，有两个值的类型通常叫Bool. - 上面的等号表示的等价关系其实是说两个类型的值的数量相等，称为类型同构$\simeq$. 和集合一样，我们也可以通过定义类型之间的同构函数来证明两个类型是同构的.
- 乘法：对应积类型（product types）. 不过更熟悉的称呼应该是元组，大多数编程语言都有的. 元组
(A, B)，如果A有$a$个值，B有$b$个，那这个元组类型就有$A\times B$个. - $1\times 2=2$：用1乘上2，
((), Bool)，确实只有两个值的((), True)和((), False). - 幂：对应函数类型
A -> B.
类型范畴
我们把类型作为对象，类型之间的函数作为态射构成一个范畴。
| 类型 | 范畴 |
|---|---|
| 0 | 终结对象 |
| 1 | 初始对象 |
| 和类型 | 余积对象 |
| 积类型 | 积对象 |
| 幂 | 函数对象 |
有上述结构的范畴称为笛卡尔闭范畴（CCC）.
递归类型？
大多数时候我们说ADT都指的是可以递归的，也就是定义类型的时候可以包括自身。在
F-代数
简单的说，我们可以用一个函子来表示一个代数结构，怎么做呢？我们先回忆一下幺半群的定义需要什么：
- 一个集合$m$
- 一个封闭的二元运算$\mu : m \times m \to m$
- 和其中的一个元素（幺元）$\eta : 1 \to m$
我们把需要的这些数据打包成一个表示幺半群的类型：
$$
\forall m. m^{m\times m}\times m^1\simeq m^{m\times m + 1}\simeq m\times m+1\to m
$$
我们可以把左边看做一个函子$F=-\times-+1$应用在类型$m$上，一个幺半群可以定义为一个对$(F, F\ m \to m)$.
使用不同的函子，我们可以推广到别的代数结构. 对于一个函子$F$，和一个态射$F\ a\to a$，$(F, F\ a\to a)$称为一个F-代数，我们可以简单的把这个态射表示这个代数.
我们现在使用函子来表示代数了，同样的现在我们考虑代数之间的同态. 还是以幺半群为例，一个从幺半群$A$到幺半群$B$的同态$f$需要满足$f(1_A)=1_B$，$f(x \times_A y)=f(x)\times_B f(y)$. 用我们的形式写写看这个条件：
- 设$f: F\ a \to a,\ g: F\ b\to b$为两个F-代数. 同态$m: a\to b$需要满足$m(f(F\ x))=g(Fm(x))$.
这对应着这张交换图：
1 | F a ---F m---> F b |
ok了，如果态射$m:a\to b$满足这个交换图的话，我们称它是从F-代数$f$到$g$的同态. 更进一步可以发现，以F-代数作为对象，F-代数之间的同态作为态射的话，又可以构成一个范畴.
- 本文作者： Frankenstein
- 本文链接： https://salty-frankenstein.github.io/blog/2025/07/10/【函数式】免费的递归类型？/
- 版权声明： 本博客所有文章除特别声明外，均采用 MIT 许可协议。转载请注明出处！