为什么 Union + Intersection 类型下子类型检查不可判定？

Saint Jerome as Scholar, El Greco, c. 1610
El Greco,《学者圣杰罗姆》, c. 1610 — 学者面前摊开的典籍层层叠叠，每翻开一页都可能引出新的注释和交叉引用，永远读不完。这和子类型检查在 union + intersection + 递归类型下的困境一样：每展开一层类型，都可能产生新的分支，新的选择，新的展开——没有尽头
这篇文章的价值：如果你用过 TypeScript，你可能遇到过类型检查卡住、报出莫名其妙的错误、或者 IDE 直接转圈圈的情况。这不是 bug——这是类型系统的根本性限制。当一个类型系统同时支持 union（|）、intersection（&）、函数类型和递归类型时，子类型检查在理论上是不可判定的。这篇文章用工程师能理解的方式，一层一层推导出这个结论：从最简单的子类型系统开始，逐步加入 union、intersection、函数逆变和递归类型，看每一步如何让问题变得更难，最终超越了算法能处理的边界。理解这个"为什么"，能帮你理解 TypeScript 为什么做出某些设计妥协，以及如何避免写出让编译器爆炸的类型。

问题定义：子类型检查是一个判定问题

先把问题说清楚。子类型检查就是回答一个 yes/no 问题：给定类型 A 和类型 B，A <: B 是否成立？

你每天都在做这件事。当你写 TypeScript 的时候：

function greet(name: string) { ... }
greet(42)  // 编译错误：number 不是 string 的子类型

编译器在背后做的就是子类型检查：number <: string？不成立，报错。

可判定意味着存在一个算法，对任意输入的 A 和 B，都能在有限步内给出正确答案。不可判定意味着不存在这样的算法——对某些输入，任何正确的算法要么永远算不完，要么给出错误答案。

这篇文章要回答的核心问题：为什么加入 union 和 intersection 类型后，子类型检查会变得不可判定？

基线：简单子类型系统是可判定的

先看最简单的情况。类型只有基本类型和函数类型：

类型 ::= number | string | A → B

子类型规则很直接：

number <: number                                // 自反性
string <: string                                // 自反性
A → B <: C → D   当且仅当   C <: A 且 B <: D   // 函数类型

函数类型的规则值得停下来说一句：参数逆变，返回值协变。直觉是——如果你需要一个"吃 Cat 吐 Animal"的函数，那"吃 Animal 吐 Cat"的函数可以替代它，因为它能吃更多（接受更广的输入），吐更精确（返回更具体的输出）。

这个系统的子类型检查显然可判定：每次应用规则都把类型拆小，没有循环，没有分支，线性时间搞定。关键在于这个过程是语法导向（syntax-directed）的——类型的结构直接告诉你用哪条规则，不需要做任何选择。

第一步复杂化：Union 和 Intersection 引入了搜索

Union 类型：析取 / OR

A | B 表示"是 A 或者是 B"。TypeScript 里到处都是：

type Result = Success | Error
type ID = string | number

子类型规则：

A <: A | B          // 左注入：A 当然是"A 或 B"
B <: A | B          // 右注入
A | B <: C  需要  A <: C 且 B <: C   // union 消除：两个分支都得满足

但反过来就麻烦了——判断 C <: A | B 时，你不能简单地检查 C <: A 或 C <: B。看这个例子：

(string | number) <: (string | number)   // ✅ 成立
(string | number) <: string              // ❌ 不成立
(string | number) <: number              // ❌ 也不成立

你需要把 C 的"成员"拆开来看，每个成员要么属于 A 要么属于 B。这不再是一步就能判定的——你需要搜索。

Intersection 类型：合取 / AND

A & B 表示"同时是 A 又是 B"。TypeScript 里常见于 mixin 模式：

type Serializable = { serialize(): string }
type Loggable = { log(): void }
type Entity = Serializable & Loggable  // 同时满足两个接口

子类型规则：

A & B <: A          // 左投影
A & B <: B          // 右投影
C <: A & B  需要  C <: A 且 C <: B   // intersection 引入

反方向也有同样的问题：A & B <: C 不能简单拆分为 A <: C 或 B <: C。

第一个关键变化：子类型检查变成了搜索问题

之前的简单系统里，每一步的推导规则是唯一确定的。现在有了 union 和 intersection，你需要做选择：

子类型检查从"确定性计算"变成了"搜索问题"。但仅仅是搜索还不够——NP 问题也是搜索问题，但仍然可判定（只是慢）。要达到不可判定，还需要更多东西。

关键一步：函数逆变让 Union 和 Intersection 互相翻转

这是整个推导链中最关键的一步。函数类型的参数位是逆变的，这个性质和 union/intersection 碰撞后，产生了一组重要的等价关系（分配律）：

  分配律（函数参数位 = 逆变位）：

  (A | B) → C   ≡   (A → C) & (B → C)     ① union 穿过参数位 → 变 intersection
  (A & B) → C   ≡   (A → C) | (B → C)     ② intersection 穿过参数位 → 变 union

  分配律（函数返回位 = 协变位）：

  A → (B | C)   ≡   (A → B) | (A → C)     ③ union 保持 union
  A → (B & C)   ≡   (A → B) & (A → C)     ④ intersection 保持 intersection

等式 ① 和 ② 是杀手锏。它们意味着：每穿过一层函数类型的参数位，union 和 intersection 就互相翻转一次。

用工程直觉理解等式 ①：一个接受 string | number 的函数，本质上是一个同时能处理 string 又能处理 number 的函数——它等价于"既是 string → C 又是 number → C"。所以参数位的 union 变成了整体的 intersection。

这让子类型判定过程中的搜索性质不断翻转：

  第 0 层：需要验证一个 AND 条件（intersection）
     │
     ▼  穿过一层函数参数
  第 1 层：变成了 OR 选择（union）
     │
     ▼  再穿过一层函数参数
  第 2 层：又翻回 AND 条件（intersection）
     │
     ▼
    ...交替下去

这不再是简单的 SAT 式搜索（纯 OR 分支），而是一个 AND-OR 交替搜索——类似博弈树（我选一步、对手选一步、我再选一步...）。博弈树的判定比 SAT 要难得多。

火上浇油：递归类型提供无限展开

到目前为止，如果所有类型都是有限大小的（没有递归），搜索树虽然复杂，但深度有界——仍然可判定（可能是 EXPTIME 甚至更高，但总能算完）。

递归类型打破了这个限制。它允许类型引用自身：

// TypeScript 中的递归类型
type Json = string | number | boolean | null | Json[] | { [key: string]: Json }

// 形式化写法
type List = μX. Nil | Cons(number, X)    // X = Nil | Cons(number, X) 的不动点

在 equi-recursive 语义（最常见的解释方式）下，递归类型等于它的一次展开：

μX. F(X)  =  F(μX. F(X))    // 可以无限展开

这意味着类型可以无限膨胀。结合前面的结论：

  1. 每穿过一层函数参数，union/intersection 就翻转一次
  2. 递归类型可以无限展开，不断产生新的函数层
  3. 每次展开都引入新的 union/intersection 分支
  4. 分支的 AND/OR 性质随展开深度交替
  5. 没有天然的终止条件

看一个具体的例子：

type T = μX. (X → X) | number

// 展开一次：
T = (T → T) | number

// 展开 T → T 中的 T：
T = (((T → T) | number) → ((T → T) | number)) | number

// 每次展开都产生新的 union，穿过 → 又变 intersection，继续...

子类型检查算法在面对这种类型时，可以无限地展开、翻转、分支。任何试图判定 A <: B 的算法，都可能在这种递归结构上永远运行下去。

终极问题：为什么能编码图灵机

前面四步给了我们所有的零件。现在看它们如何组装成图灵完备的计算。

图灵机需要什么 vs 类型系统提供了什么

图灵机组件类型系统对应物谁提供的
有限状态不同的类型构造（union 的不同分支）Union 类型
无限带子递归类型的无限展开递归类型
状态转移函数函数逆变 + union/intersection 分配律函数类型 + 逆变
分支判断AND-OR 交替搜索Union + Intersection + 逆变
计算步骤子类型检查的一步推导子类型规则

编码的直觉

核心思想是构造两个递归类型 A 和 B，使得 A <: B 成立当且仅当某个图灵机停机。

每次子类型检查展开一步递归类型，就相当于图灵机执行一步。如果图灵机不停机，子类型检查就永远算不完。

标准归约路线

经典证明通常通过两步归约：

  停机问题（已知不可判定）
     │
     │  归约到
     ▼
  Post 对应问题 (PCP)
  给定字符串对 (u₁,v₁), ..., (uₙ,vₙ)
  是否存在序列 i₁,...,iₖ 使得
  u_{i₁}...u_{iₖ} = v_{i₁}...v_{iₖ} ?
     │
     │  归约到
     ▼
  子类型检查问题
  A <: B ?

PCP 到子类型检查的编码：

验证直觉：去掉任何一个组件会怎样？

如果上面的分析是对的，那么去掉任何一个关键组件都应该让问题重新变得可判定。事实确实如此：

配置可判定？原因
只有 Union，没有 Intersection可判定没有 intersection，函数参数位不会把 union 翻转成 intersection，AND-OR 交替不出现
只有 Intersection，没有 Union通常可判定更容易控制，虽然某些组合（如 bounded quantification）可能仍有问题
有 Union + Intersection，没有递归可判定所有类型有限大，搜索树有限深度。可能是 EXPTIME，但总能终止
有 Union + Intersection + 递归，没有函数类型可判定没有逆变位置，union 和 intersection 不会互相翻转，退化为集合包含检查

结论：不可判定需要四个组件的共同作用，缺一不可。

  Union（提供 OR 分支）
    + Intersection（提供 AND 分支）
    + 函数类型的逆变（让 OR ↔ AND 互相翻转）
    + 递归类型（让这个过程无限延续）
    ────────────────────────────────
    = 可以编码图灵机 → 不可判定

完整因果链

  WHY-0: 停机问题不可判定
            ↓
  WHY-1: 任何能编码图灵机的形式系统中的判定问题都不可判定
            ↓
  WHY-2: Union + Intersection + 函数类型 + 递归类型能编码图灵机
            ↓ 因为
  WHY-3: Union 编码 OR 选择，Intersection 编码 AND 合取
            ↓ 加上
  WHY-4: 函数参数的逆变让 union ↔ intersection 互相翻转
            ↓ 使得
  WHY-5: 子类型检查变成 AND-OR 交替搜索
            ↓ 再加上
  WHY-6: 递归类型让展开过程没有终止点
            ↓ 最终
  WHY-7: 子类型检查可以编码任意图灵机 → 不可判定

实际的类型系统怎么应对？

理论上不可判定，但我们每天用的 TypeScript、Flow、Scala 都活得好好的。它们怎么做到的？本质上是放弃了"完备性"或"完全的递归"来换取可判定性。

策略一：不完备但可靠（TypeScript 的做法）

TypeScript 的子类型检查算法是 sound but incomplete——它不会接受错误的子类型关系（可靠），但可能拒绝一些实际成立的子类型关系（不完备）。

// TypeScript 的子类型检查在某些情况下会放弃
type A = { x: string } & { y: number }
type B = { x: string, y: number }
// A <: B 且 B <: A，TypeScript 能处理这个

// 但对于深度嵌套的递归 + union + intersection 组合
// 编译器可能直接报错或者超时

实践中的表现：如果你写过复杂的 TypeScript 类型体操（conditional types + infer + 递归），你可能见过 Type instantiation is excessively deep and possibly infinite 这个错误。这就是 TypeScript 的深度限制在起作用——当递归展开超过一定深度（通常是 50 层），直接停止。

策略二：语义子类型（CDuce、Ballerina 的做法）

把类型解释为值的集合，子类型就是集合包含。通过限制递归类型的形式来恢复可判定性：

策略三：限制 union/intersection 的出现位置

有些类型系统只允许 union/intersection 出现在特定位置——比如只能出现在顶层，不能嵌套在函数参数里。这直接阻断了逆变翻转的链条。

策略四：Iso-recursive 代替 Equi-recursive

Iso-recursive 类型需要显式的 fold/unfold 操作才能展开递归。每次展开都由程序员主动触发，而不是类型检查器自动无限展开。这限制了展开深度。

策略五：MLsub 的巧妙限制

Dolan 和 Mycroft 在 2017 年的 MLsub 系统展示了一种聪明的方法：通过限制 union 和 intersection 只能出现在特定的"极性（polarity）"位置——union 只在协变位，intersection 只在逆变位——完全消除了 AND-OR 交替的可能，得到了一个可判定且高效的系统。

对工程实践的启示

理解了不可判定的根源，可以指导我们写出更"友好"的类型：

参考文献