和类型

和类型表达“这里有一份 $A$，或者有一份 $B$，并且值自己携带证据说明是哪一种”。标签是定义的关键：没有标签的集合并集在两侧重叠时无法知道应采用哪个分支的处理逻辑。使用和类型必须覆盖所有可能标签，因此模式匹配把运行时分支与静态穷尽性检查结合起来。它不是把两种类型的字段都放在一起，而是一次只选择一个构造器。

和类型 $A+B$ 在运行时公开标签，使用者可模式匹配并知道当前是哪一分支；存在类型公理库存在类型Existential type · Existentially quantified type隐藏一个见证类型及其实现值，只允许客户端通过公开接口使用该表示的量化类型。把某个见证类型隐藏在包内，只暴露满足接口的操作。二者都能封装异构值，但一个暴露有限选择，一个刻意抽象具体表示。

可选值可定义为 $\mathrm{Option}(A)=1+A$：None 使用单位类型一侧，Some(a) 使用 $A$ 一侧。除法结果也可表示为 $\mathrm{Error}+\mathbb{Q}$，调用者通过 case 明确处理除零与正常商。

边界是未经标记的“联合内存”：若只存一段比特而不记录当前分支，读取者可能用错误类型解释数据。另一个常见错误是漏掉一个模式分支；类型规则要求两个分支都产生同一结果类型 $C$，否则整个 case 无法定型。

和类型是枚举、变体、错误返回和抽象语法构造器的基础。异常语义公理库异常语义Exception semantics把正常返回与异常传播作为不同控制结果描述的语义。可显式化为正常结果与错误的和；有限构造子的选择、字段积与可选递归如何统一成代数数据类型公理库代数数据类型Algebraic data type · Algebraic datatype以有限构造子的和、每个构造子字段的积以及可选递归组合数据形状的类型。，由汇总页集中说明，本页保留二选一的引入、消去与标签边界。

在Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。下，$A+B$ 对应析取 $A\vee B$：证明必须说明成立的是哪一侧，而使用该证明需要分别处理两种情况。它与积类型公理库积类型Product type其值由两个分量组成并支持投影的类型。构成类型层面的“选择”与“并有”。