归纳类型

约定. 在本文中,

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

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

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

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

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

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

1定义

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

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

简单类型

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

定义 1.1 (数据类型). 令 $\Gamma ,x:X⊢D(x):\mathcal{U}$ 为一类型. 接下来将它的构造规则由一组如下形式的函数符号给出 (称为构造子): $$\frac{\Gamma ,x:X,D:X\to \mathcal{U}⊢u:C_i}{\Gamma ,x:X⊢{\mathrm{con}}_i(u):D(x)}$$其中, $C_i$ 是一个类型, 它可以引用当前正在被定义的类型 $D(x)$ 自身, 以及其中涉及的变量 $x:X$. 用这种方式定义的类型叫做数据类型.

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

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

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

•	$D(x)$ 对应自然数类型本身 $\mathbb{N}$, 这意味着 $X=1$,
•	$C_1$ 不包含任何数据, 因此 $C_1=1$,
•	${\mathrm{con}}_1(u)$ 对应自然数 $0$, 类型为 $1\to \mathbb{N}$, 和标准定义中的 $\mathbb{N}$ 等价,
•	$C_2(x)$ 递归地引用自身, 对应 $\mathbb{N}$,
•	${\mathrm{con}}_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$ 的定义不能不受限制地引用 $D(x)$, 它必须确保自己是如下形式: $$C=\prod _{i:I}E(i)$$其中 $I$ 不能引用 $D$, 然后 $E(i)$ 满足如下条件:

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

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

例 1.4. 如下类型作为 $D(x)$ 的构造子的参数类型是严格正的. $$C=X\to (X\to D(x))$$其中 $X$ 是一个具体的类型, 和 $D$ 无关. 原因是我们可以将它看作 ${\prod }_{i:I}E(i)$ 的特例, 其中 $I=1$, $E(i)=X\to (X\to D(x))$.

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

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

简单类型

将上述所有定义中的 $X$ 换成宇宙或者它们的积就得到了简单类型论中的归纳类型. 自然数类型就是一个简单类型的归纳类型, 因为单位类型可以看作零元的积.

宇宙层级

在有宇宙层级时, 若 $D(x):{\mathcal{U}}_k$, 那么必须也有 $C_i:{\mathcal{U}}_k$. 换言之, 类型本身所在的层级必须和构造子的参数所在的层级匹配.

类型签名

很多时候需要考虑多个参数的归纳类型, 可以用积类型来将这些参数类型拼起来: $D(x)$ 中 $x:X_1\times X_2\times \cdots \times X_n$. 其中 $X_i$ 是任意类型 (在简单类型的情况中, 可以看作是 $\forall i,X_i=\mathcal{U}$). 为了直观, 这种情况下会写作$$D:X_1\to X_2\to \cdots \to X_n\to \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 • 日文 構成子