积 (类型论)

积类型是积集在类型论中的类比, 它在简单类型论和依值类型论里都可以定义, 且定义是一样的. 注意积类型不是 $\Sigma$ 类型, 即使有时我们认为积类型是 $\Sigma$ 类型的特例.

在类型论中, 积类型的对偶是不交并.

1类型规则

类型 $A$ 和 $B$ 的积记作 $A\times B$.

$$\frac{\Gamma ⊢A\mathrm{type}\Gamma ⊢B\mathrm{type}}{\Gamma ⊢(A\times B)\mathrm{type}}$$

以下规则基本就是模仿范畴论中积的泛构造.

构造规则

$$\frac{\Gamma ⊢u:A\Gamma ⊢v:B}{\Gamma ⊢⟨u,v⟩:A\times B}$$

可以直接将 $A\times B$ 视为由如上构造子生成的归纳类型, 也可以单独给出消去规则.

消去规则

积类型的消去规则有两种风格:

$$\frac{\Gamma ⊢u:A\times B}{\Gamma ⊢u.1:A\text{and}\Gamma ⊢u.2:B}$$

其中:

$$\begin{gathered} ⟨u,v⟩.1=u \\ ⟨u,v⟩.2=v \end{gathered}$$

另一种风格是通过函数类型定义, 也就是 $A\times B$ 作为归纳类型的情况下的消去规则:

$$\frac{\Gamma ⊢C\mathrm{type}\Gamma ⊢u:A\times B\Gamma ⊢f:A\to (B\to C)}{\Gamma ⊢\text{uncurry}(f,u):C}$$

其中:

$$\text{uncurry}(f,⟨u,v⟩)=f(u)(v)$$

这种思路非常接近 Curry 化和积类型的$\lambda$ 编码. 两者的区别在于极性不同.

2范畴语义

•	在简单类型论的范畴语义中, 积类型对应积对象.

•	在依值类型论的范畴语义中, 积类型对应俯范畴里的积, 也就是拉回.

术语翻译

积类型 • 英文 product type • 法文 type produit • 拉丁文 typus productus