类型系统中的和类型与变体类型详解

### 类型系统中的和类型与变体类型详解 在编程中，我们常常需要处理不同类型值的集合。例如，二叉树的节点可以是叶子节点，也可以是有两个子节点的内部节点；列表单元可以是空列表，也可以是包含头部和尾部的单元。为了支持这种编程方式，类型理论中引入了变体类型。在深入探讨通用变体类型之前，我们先从二元和类型这个简单的情况开始。 #### 1. 二元和类型 二元和类型描述了一个由两个给定类型的值组成的集合。例如，我们可以定义两种不同的地址类型： ```plaintext PhysicalAddr = {firstlast:String, addr:String}; VirtualAddr = {name:String, email:String}; ``` 如果我们想统一处理这两种地址记录，就可以引入和类型： ```plaintext Addr = PhysicalAddr + VirtualAddr; ``` 这个和类型 `Addr` 的元素要么是 `PhysicalAddr` 类型，要么是 `VirtualAddr` 类型。我们可以通过标记组件类型的元素来创建和类型的元素。例如，如果 `pa` 是一个 `PhysicalAddr` 类型的值，那么 `inl pa` 就是一个 `Addr` 类型的值。这里的 `inl` 和 `inr` 可以看作是将元素“注入”到和类型左右组件的函数： ```plaintext inl : PhysicalAddr → PhysicalAddr+VirtualAddr inr : VirtualAddr → PhysicalAddr+VirtualAddr ``` 但在我们的表示中，它们并不被当作函数处理。一般来说，类型 `T1+T2` 的元素由标记为 `inl` 的 `T1` 元素和标记为 `inr` 的 `T2` 元素组成。 为了使用和类型的元素，我们引入了 `case` 构造，它可以让我们区分一个值是来自和类型的左分支还是右分支。例如，我们可以从 `Addr` 类型的值中提取名称： ```plaintext getName = λa:Addr. case a of inl x ⇒ x.firstlast | inr y ⇒ y.name; ``` 当参数 `a` 是标记为 `inl` 的 `PhysicalAddr` 时，`case` 表达式会选择第一个分支，将变量 `x` 绑定到该 `PhysicalAddr`，并返回 `x` 的 `firstlast` 字段。如果 `a` 是标记为 `inr` 的 `VirtualAddr`，则选择第二个分支并返回 `y` 的 `name` 字段。因此，整个 `getName` 函数的类型是 `Addr→String`。 下面是和类型相关的语法、求值规则和类型规则： - **新语法形式** ```plaintext t ::= ... | inl t tagging (left) | inr t tagging (right) | case t of inl x⇒t | inr x⇒t case v ::= ... | inl v tagged value (left) | inr v tagged value (right) T ::= ... | T+T sum type ``` - **新求值规则** ```plaintext t -→ t′ case (inl v0 ) of inl x1⇒t1 | inr x2⇒t2 -→ [x1 , v0]t1 (E-CaseInl) case (inr v0 ) of inl x1⇒t1 | inr x2⇒t2 -→ [x2 , v0]t2 (E-CaseInr) t0 -→ t′0 case t0 of inl x1⇒t1 | inr x2⇒t2 -→ case t′0 of inl x1⇒t1 | inr x2⇒t2 (E-Case) t1 -→ t′1 inl t1 -→ inl t′1 (E-Inl) t1 -→ t′1 inr t1 -→ inr t′1 (E-Inr) ``` - **新类型规则** ```plaintext Γ ⊢ t : T Γ ⊢ t1 : T1 Γ ⊢ inl t1 : T1+T2 (T-Inl) Γ ⊢ t1 : T2 Γ ⊢ inr t1 : T1+T2 (T-Inr) Γ ⊢ t0 : T1+T2 Γ, x1:T1 ⊢ t1 : T Γ, x2:T2 ⊢ t2 : T Γ ⊢ case t0 of inl x1⇒t1 | inr x2⇒t2 : T (T-Case) ``` #### 2. 和类型与类型唯一性 纯 λ→ 类型关系的大多数属性可以扩展到包含和类型的系统，但有一个重要的属性不成立，即类型唯一性定理。问题出在标记构造 `inl` 和 `inr` 上。例如，根据类型规则 `T-Inl`，一旦我们证明 `t1` 是 `T1` 的元素，就可以推导出 `inl t1` 是 `T1+T2` 的元素，其中 `T2` 可以是任意类型。这意味着 `inl 5` 既可以是 `Nat+Nat` 类型，也可以是 `Nat+Bool` 类型，甚至可以是无限多种其他类型。类型唯一性的失败意味着我们不能像之前处理其他特性那样，简单地通过“从下往上读取规则”来构建类型检查算法。 此时，我们有以下几种选择： 1. **复杂化类型检查算法**：让算法“猜测” `T2` 的值。具体来说，我们先不确定 `T2` 的值，然后在后续过程中尝试确定它。这种技术将在类型重构中详细探讨。 2. **细化类型语言**：使所有可能的 `T2` 值能够以统一的方式表示。这将在讨论子类型时进行探索。 3. **要求程序员提供显式注释**：这是最简单的方法，而且在实际的语言设计中，这些显式注释通常可以“搭载”在其他语言构造上，从而基本上不可见。我们目前采用这种方法。 为了实现类型唯一性，我们对语法和规则进行了扩展。现在，我们使用 `inl t as T` 或 `inr t as T` 的形式，其中 `T` 指定了注入元素所属的整个和类型。扩展后的语法、求值规则和类型规则如下： - **新语法形式** ```plaintext t ::= ... | inl t as T tagging (left) | inr t as T tagging (right) v ::= ... | inl v as T tagged value (left) | inr v as T tagged value (right) ``` - **新求值规则** ```plaintext t -→ t′ case (inl v0 as T0 ) of inl x1⇒t1 | inr x2⇒t2 -→ [x1 , v0]t1 (E-CaseInl) ca ```