W 类型

约定. 在本文中,

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

$\mathcal{W}$ 类型是 Martin-Löf 类型论中的一个特殊的归纳类型, 大多数归纳类型都等价于它的某种特化. 它的动机是将值视为某种 “树状结构”, 这种树之间的包含关系构成了一种良基关系. 事实上归纳类型的通用定义差不多就长这样. 从范畴论的视角, 它是多项式函子的始代数.

在数学研究中, 时常会有 “X 是 Y 的特殊情况” 这样的发现, 然后关于 Y 的研究就会变得比 X 更通用. 在类型论中, 如果某个类型 X 等价于另一个类型 Y 的特化, 那么在使用 X 的地方全部改为使用 Y 的特化的话, 依然能做原本能做的数学, 但底层使用的定义就更少了, 从而使得底层理论更简洁. $\mathcal{W}$ 类型正是这样的一个非常通用的类型. 例如, 某个归纳类型可能有如下数据:

•	类型本身 $D:\mathcal{U}$,
•	构造子 ${\mathrm{con}}_i:C_i\to D,i\in [0,n]$, 其中 $C_i$ 可以使用 $\Pi$ 类型和 $\Sigma$ 类型也可以在满足严格正性的情况下使用 $D$.

接下来我们将它转化为一个单参数单构造子的等价的归纳类型:

•	首先处理无交并类型: 考虑 $k$ 个类型的无交并, 可以定义一个有 $k$ 个实例的类型 $K$, 再用一个函数 $m:K\to \mathcal{U}$ 表示这些类型的并.
•	任何多元函数都可以用 Curry 化的思想转化为一元函数, 于是我们可以认为 $C_i$ 中仅包含一元函数, 其中返回类型中允许出现 $D$, 参数中不允许.
•	用无交并将多个函数合并为单个函数. 现在可以认为 $C_i$ 只能是一种返回 $D$ 的一元函数或者普通类型了.
•	多个构造子可以直接取它们的无交并变成单个构造子.

事实也是如此, $\mathcal{W}$ 类型只需要一个构造子就可以表达丰富多彩的归纳类型.

在集合论模型中, 可以证明 $\mathcal{W}$ 类型存在, 但在类型论的研究中, 一般是将 $\mathcal{W}$ 类型作为底层构造引入的, 类似 $\Pi$ 类型和 $\Sigma$ 类型. 在观测类型论中就是这样处理的.

$\mathcal{W}$ 类型有归纳类型和归纳族的版本. 它的对偶是余归纳的 $\mathcal{M}$ 类型.

1类型规则

$$\frac{\Gamma ⊢A\Gamma ,x:A⊢B}{\Gamma ⊢\underset{x:A}{W}B}$$

这个形成规则最好配合构造规则一起理解.

构造规则

$$\frac{\Gamma ⊢a:A\Gamma ⊢t:B[x\mapsto a]\to \underset{x:A}{W}B}{\Gamma ⊢\mathsf{sup}(a,t):\underset{x:A}{W}B}$$

其中, 类型 $A$ 的实例数量代表了它对应的归纳类型有多少个构造子, 而 $t$ 代表了对应构造子接受的参数.

假设我们需要用 $\mathcal{W}$ 类型来模拟有两个构造子 ${\mathrm{con}}_1,{\mathrm{con}}_2$ 的类型, 并假设经过一番操作后我们已经让这两个构造子都只需要接受一个参数. 那么令 $A$ 为有两个实例 $a_1,a_2$ 的类型, 于是 $\mathsf{sup}(a_1,x)$ 就代表了 ${\mathrm{con}}_1(x)$, $\mathsf{sup}(a_2,x)$ 则代表了 ${\mathrm{con}}_2(x)$.

消去规则

此处直接给出依值类型的版本. 为了简洁, 以下直接将 $\underset{x:A}{W}B$ 简写为 $\mathcal{W}$.

$$\frac{\Gamma ⊢C:\mathcal{W}\to \mathcal{U}\Gamma ⊢w:\mathcal{W}\Gamma ,x:A,\boxed{u:B\to \mathcal{W}},\boxed{v:{\prod }_{y:B}C(u(y))}⊢c(x,u,v):C(\mathsf{sup}(x,u))}{{\mathrm{rec}}_W(w,c):C(w)}$$

其中:

$${\mathrm{rec}}_W(\mathsf{sup}(x,u),c)=c(x,u,\lambda y.{\mathrm{rec}}_W(u(y),c)):C(w)$$

2范畴语义

回顾其类型规则$$\frac{\Gamma ⊢A\Gamma ,x:A⊢B}{\Gamma ⊢\underset{x:A}{W}B}$$在依值类型论的范畴语义中, 用一个态射 $p:A\to \Gamma$ 表示一族依赖于 $\Gamma$ 的类型, 可以看作纤维化中依赖于底空间的一族纤维. 而 $\Gamma ,x:A⊢B$ 则表示为 $q:B\to A$, 即纤维化上的纤维化. 这些数据给出了一个复合函子$$\mathcal{C}/\Gamma \stackrel{(p\circ q{)}^{\ast }}{\to }\mathcal{C}/B\stackrel{{\Pi }_q}{\to }\mathcal{C}/A\stackrel{{\Sigma }_p}{\to }\mathcal{C}/\Gamma .$$这个复合函子称为多项式函子. $\mathcal{W}$ 类型是多项式函子的 “最小” 不动点, 这在范畴论中的严格表述是自函子上的代数.