归纳类型

约定. 在本文中,

• $\overline{X}$ 代表 $X_1,X_2,\cdots ,X_n$ 这样的列表的简写.

归纳类型 (又叫代数数据类型) 是一类类型, 在简单类型论和依值类型论里面有各自的版本. 大致来说, 归纳类型就是可以在它上面用归纳法的类型, 它由一组生成元 (又叫构造子) 指定, 并且配备一个函数来进行归纳 (又叫消去子, 因为这个函数对应了消去规则), 比如自然数类型就是一种归纳类型.

归纳类型的构造子的类型有严格限制. 若生成元的类型引用了这个归纳类型自身, 那么它需要确保这些引用不能出现在某些位置. 这是为了确保类型论的正规性.

归纳类型在范畴语义上对应一种有始代数的自函子.

归纳类型有非常多种方式推广, 比如高阶归纳类型、归纳族、归纳递归、互归纳等. 推广方式可以从语法的角度出发, 也可以从语义的角度出发.

归纳类型的对偶是余归纳类型.

1定义

由于归纳类型推广的方式太多, 导致太多的类型可以被称作归纳类型, 且这个概念随着时间在不断变化, 因此很难给出普适的定义.

以下定义尽可能在不同类型论中给出一种足够通用的版本的归纳类型, 仅供参考.

简单类型

首先我们给出基本的语法框架, 再在此之上给出一些必要的限制.

定义 1.1 (数据类型). 令 $D(\overline{X})$ 为一类型, 其中 $X_i$ 是类型参数, 或者说变量. 接下来将它的构造规则由一组如下形式的函数符号给出 (称为构造子): $$\frac{\Gamma ⊢u:C_i(\overline{X})}{\Gamma ⊢\mathrm{co}{\mathrm{n}}_{\mathrm{i}}(u):D(\overline{X})}$$其中, $C_i(\overline{X})$ 是一个类型, 它可以引用 $D(\overline{X})$ 自身, 以及其中涉及的类型变量. 用这种方式定义的类型叫做数据类型.

数据类型的消去规则是类似这样的函数 (称为消去子): 给定类型 $A$、一组函数 $\overline{f}$, 其中$$f_i:C_i(\overline{X})\to A$$代表 “处理第 $i$ 个构造规则” 的函数, 然后再给出一个 $u:D(\overline{X})$ 类型的实例, 返回 $A$, 写法如下: $${\mathrm{rec}}_{D(\overline{X})}(\overline{f},u):A$$数据类型的消去也常常使用模式匹配的语法书写. 其中, $f_i$ 可以引用 ${\mathrm{rec}}_{D(\overline{X})}$.

计算规则便是将 $u$ 根据它具体的构造规则, 选择合适的函数处理.

自然数类型就是一种数据类型, 定义如下 (注意区分下文中的各种数字: $0$ 代表自然数, $1$ 代表单位类型):

•	$D(\overline{X})=\mathbb{N}$
•	$C_1(\overline{X})=1$
•	$\mathrm{co}{\mathrm{n}}_1(u)=0$, 类型为 $1\to \mathbb{N}$, 和标准定义中的 $\mathbb{N}$ 等价.
•	$C_2(\overline{X})=\mathbb{N}$
•	$\mathrm{co}{\mathrm{n}}_2(u)=s(u)$, 类型为 $\mathbb{N}\to \mathbb{N}$

这样的递归类型非常通用, 而且允许不太有意义的消去规则, 例如我们可以定义 $f_i(x)={\mathrm{rec}}_D(\overline{f},\mathrm{co}{\mathrm{n}}_{\mathrm{i}}(x))$, 根据计算规则, 表达式 $f(\mathrm{co}{\mathrm{n}}_{\mathrm{i}}(x))$ 不存在更简单的形式, 这给出了正规性的反例.

为了解决这个问题, 需要引入两个限制:

命题 1.2 (结构递归). $f(x)$ 的定义不能不受限制地引用 ${\mathrm{rec}}_D$, 它必须确保每次引用的时候, 会传入一个满足如下规定 (称之为 “更小”) 的参数:

•	$x$ 的子表达式, 或者.
•	对一个更小的表达式的函数应用.

满足这样的限定条件的消去规则叫做结构递归.

命题 1.3 (严格正性).

主条目: 严格正性

$C(\overline{X})$ 的定义不能不受限制地引用 $D(\overline{X})$, 它必须确保自己是如下形式: $$C(\overline{X})=E_1\times E_2\times \cdots \times E_n$$其中, $E_i$ 是满足如下条件的类型:

•	不 (直接或间接) 引用 $D$, 或者
•	形如 $F\to D$, 其中 $F$ 不引用 $D$.

这样的定义出的类型 $D$ 是严格正的.

例 1.4. 如下类型作为 $D$ 的构造子的参数类型是严格正的. $$C=X\to (X\to D)$$其中 $X$ 是一个具体的类型, 和 $D$ 无关.

容易验证自然数类型的定义满足这两个限制.

定义 1.5 (归纳类型). 将 1.1 中定义的类型加上 1.2,1.3 的限定条件得到的类型就是简单类型情况的归纳类型.

依值类型

将上述所有函数类型换成$\Pi$ 类型就得到了依值类型中的归纳类型的雏形, 但并不完整. 一般还会允许在 $D(\overline{X})$ 中, $X$ 不仅可以包含类型, 还可以包含值. 为了直观, 一般直接写作$$D:X_1\to X_2\to \cdots \to X_n\to \mathcal{U}$$其中 $X_i$ 是任意类型 (在简单类型的情况中, 可以看作是 $\forall i,X_i=\mathcal{U}$). 这意味着 $D$ 在给足所有参数后, 变成一个类型. 但这并不意味着 $D$ 变成了一个函数, 相反, 它更接近一种$\Sigma$ 类型: 它不会因为有了参数就像函数一样被消去, 而是会将这些参数收集起来提供给构造子.

2性质

•	关于归纳类型的最简形式, 见$W$ 类型.

•	关于归纳类型的唯一性规则, 参见该文.

归纳类型的定义基本上取决于它的类型和构造子, 而消去子可以由构造子推导得出.

3例子

•	无交并类型是比较简单的一种不递归的归纳类型.
•	自然数类型是比较简单的一种归纳类型.
•	积类型同时是归纳类型和余归纳类型.

4范畴语义

一言蔽之, 归纳类型的范畴语义是某种余极限, 非常接近某种自由代数.

首先考虑简单类型的情况: 此时类型是某范畴 $\mathcal{C}$ 里的对象, 实例就是态射, 暂时不考虑类型带参数的情况. 一个归纳类型在定义的时候含有如下数据:

•	被定义的归纳类型本身, 即 $D$
•	它的所有构造子, $\mathrm{co}{\mathrm{n}}_{\mathrm{i}}:C_i\to D$. 此时我们忽略构造子的名字, 只用下标区分它, 毕竟名字只是写给人看、便于区分用的.

构造子可以视为一组万剑归宗的态射:

$$C_{1}D{C}_2\cdots C_n$$

对 $\overline{C}$ 取余积就可以将这些构造子全部整合起来, 打包成一个态射. 这就是归纳类型的构造子的范畴语义. 具体来说, 考虑如下自函子:

$$\begin{array}{rl}F& :\mathcal{C}\to \mathcal{C}\\ F& (X)=\coprod _{i=1}^n{C}_i\end{array}$$

该类型的构造子对应一态射 $c:F(X)\to X$. 注意, $C_i$ 在满足严格正的条件下是可以引用 $X$ 的.

满足等式 $F$ 的始代数 $X$ 就是该归纳类型的范畴语义.

5推广

•	高阶归纳类型允许构造子构造出该类型上的相等类型的实例.
•	归纳族允许构造子构造出该类型的特化.
•	归纳递归允许构造子中出现一些对当前类型进行消去的函数.
•	索引类型允许构造子构造出该类型对某一组参数的特化.
•	互归纳允许构造子构造出该类型对某一组参数的特化, 且这一组参数的类型用到了当前归纳类型. 即: 有 $A:\mathcal{U},B:A\to \mathcal{U}$ 两归纳类型, 后者是索引类型, 且 $A$ 的构造子引用 $B$.

术语翻译

归纳类型 • 英文 inductive type • 日文 帰納的型

构造子 • 英文 constructor • 日文 構成子