形式陈述

给定类型 $A,B$$A,B$，和类型 $A+B$$A+B$ 由带标签的左、右注入构成：

$$ \frac{\Gamma\vdash t:A}{\Gamma\vdash \operatorname{inl}t:A+B}, \qquad \frac{\Gamma\vdash t:B}{\Gamma\vdash \operatorname{inr}t:A+B}. $$$$\frac{\mathrm{\Gamma }⊢t:A}{\mathrm{\Gamma }⊢\mathrm{inl}t:A+B},\frac{\mathrm{\Gamma }⊢t:B}{\mathrm{\Gamma }⊢\mathrm{inr}t:A+B}.$$

消去形式是穷尽分支的 case 分析：若 $t:A+B$$t:A+B$，且在 $x:A$$x:A$ 时两分支都产生 $C$$C$，在 $y:B$$y:B$ 时也产生 $C$$C$，则整个 case 表达式类型为 $C$$C$。计算规则选择与注入标签相符的分支。

直觉

一个和类型值只包含两种备选之一，同时保留标签以说明是哪一支，因此消费者必须分别处理所有可能。

例子与边界

Result = Value + Error、可选值 1+A 和代数数据类型的构造器都来自和类型。即使 $A$$A$ 与 $B$$B$ 含相同底层值，inl a 与 inr a 仍不同。和类型不是无标签集合并集，也不等于子类型联合；标签使 case 分析具有确定语义并支持规范形证明。

推论与应用

和类型精确表达变体、错误返回和有限选择。与积类型、递归类型组合可定义列表和树；在 Curry–Howard 对应中，$A+B$$A+B$ 对应逻辑析取。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Ch. 11, variants and sums。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Ch. 12, sum types。