无交并 (类型论)

无交并类型 (又叫余积类型) 是集合的无交并在类型论中的类比, 它在简单类型论和依值类型论里都可以定义. 在类型论中, 无交并的对偶是积类型.

1类型规则

类型 $A$ 和 $B$ 的无交并记作 $A+B$.

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

以下规则基本上是模仿余积的万有性质.

构造规则

$$\frac{\Gamma ⊢u:A}{\Gamma ⊢\mathrm{inl}u:A+B}\frac{\Gamma ⊢u:B}{\Gamma ⊢\mathrm{inr}u:A+B}$$

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

消去规则

简单类型的消去规则:

$$\frac{\Gamma ⊢a:A\to C\Gamma ⊢b:B\to C\Gamma ⊢u:A+B}{\Gamma ⊢{\mathrm{rec}}_{+}(a,b,u):C}$$

简单类型的计算规则:

$$\begin{gathered} {\mathrm{rec}}_{+}(a,b,\mathrm{inl}u)=a(u):C \\ {\mathrm{rec}}_{+}(a,b,\mathrm{inr}u)=b(u):C \end{gathered}$$

2范畴语义

在简单类型论的范畴语义中, 无交并类型对应 (弱化的) 余积对象. 而在依值类型论的范畴语义中, 无交并类型对应 (弱化的) 俯范畴里的余积, 注意这不是推出.

术语翻译

无交并类型 • 英文 disjoint union type • 法文 type d’union disjointe • 拉丁文 typus summae disiunctae

余积类型 • 英文 coproduct type • 法文 type coproduit • 拉丁文 typus coproductus