归纳族

归纳族 (又叫广义代数数据类型、指标类型) 是归纳类型在依值类型论中的推广, 它允许构造子的返回类型仅仅是归纳类型对于它参数的一组实例的特化, 因此归纳族的类型中总是有参数.

例如, 考虑如下类型:

•	类型定义为 $\mathrm{Fin}:\mathbb{N}\to \mathcal{U}$, 有一个自然数类型参数,
•	构造子 $f0:\mathrm{Fin}1$,
•	构造子 $\mathrm{fs}:{\prod }_{n:\mathbb{N}}\left(\mathrm{Fin}n\to \mathrm{Fin}(sn)\right)$.

而它的消去规则只用考虑可能的构造子, 比如 $\mathrm{Fin}0$ 对这两个构造子都不适合, 这个类型拥有如下特征:

•	$\mathrm{Fin}0$ 没有任何可用的构造子, 因此这是空类型.
•	$\mathrm{Fin}1$ 有一个构造子可用 $f0$, 因为若存在 $n$ 使得 $\mathrm{fs}n:\mathrm{Fin}1$, 那么 $n:\mathrm{Fin}0$, 与前文矛盾. 这可以看作单位类型.
•	$\mathrm{Fin}2$ 两个构造子均可用, 一共两个不同的实例.
•	$\mathrm{Fin}3$ 一共三个不同的实例.
•	事实上, 对于任意 $n:\mathbb{N}$, $\mathrm{Fin}n$ 一共有 $n$ 个不同的实例.

以上类型被称为有限集合类型, 是典型的归纳族. “族” 这个名字是因为可以把 $\mathrm{Fin}$ 看作定义了一族类型的函数.

1定义

定义 1.1. 考虑依值类型论中的归纳类型$$\Gamma ⊢D:A\to \mathcal{U}$$和它的构造子$$\Gamma ⊢\mathrm{co}{\mathrm{n}}_{\mathrm{i}}:\prod _{x:A}\prod _{y_i:C_i}D(x)$$若将构造子的类型定义改为$$\frac{\Gamma ,y_i:C_i⊢u_i:A}{\Gamma ⊢\mathrm{co}{\mathrm{n}}_{\mathrm{i}}:{\prod }_{y_i:C_i}D(u_i)}$$换言之, 不再以 $x:A$ 为参数, 而是去指定一个具体的值 $u_i:A$, 那么这便是一个归纳族, 参数类型 $A$ 叫做它的指标.

这个定义可以借助 $\Sigma$ 类型非常简单地推广到多参数的情形.

2例子

Martin-Löf 类型论中的相等类型可以视为一种归纳族. 最简单的定义如下:

•	类型定义 $\mathrm{Id}:\left({\sum }_{A:\mathcal{U}}A\times A\right)\to \mathcal{U}$
•	构造子 $\mathrm{refl}:{\prod }_{x:{\sum }_{A:\mathcal{U}}A}\mathrm{Id}(x.1,x.2,x.2)$, 但往往采用更直观的等价版本 $\mathrm{refl}:{\prod }_{A:\mathcal{U}}{\prod }_{x:A}\mathrm{Id}(A,x,x)$

此外, 异质相等也可以被定义为归纳族:

•	类型部分 $\mathrm{JM}:\left({\sum }_{A:\mathcal{U}}{\sum }_{B:\mathcal{U}}A\times B\right)\to \mathcal{U}$
•	构造子 $\mathrm{refl}:{\prod }_{A:\mathcal{U}}{\prod }_{x:A}\mathrm{JM}(A,A,x,x)$

3相关概念

•

简化归纳族.

•	Ford 化解释了如何借助相等类型将一般的归纳族转化为等价的归纳类型.

术语翻译

归纳族 • 英文 inductive family

广义代数数据类型 • 英文 generalized algebraic data type

指标类型 • 英文 indexed type