类型检查算法：证明检查算法的机械实现

上一篇给出了 STLC 的类型规则。规则本身只描述了"什么样的程序合法"，并没有说"怎样判断合法"。本篇把这个判断过程写成一段可运行的 Python 程序，约 200 行。

读完这段代码之后，"类型检查 = 证明检查"会从概念对位落到一段能跑出真实输出的事实。系列主线问题"为什么编译通过就是定理得证"的第一层——证明可被机械检查——也在这里被实证。

算法策略：从规则到代码

上一篇的规则形如：

1
2
3

  Γ ⊢ e1 : τ1 → τ2     Γ ⊢ e2 : τ1
────────────────────────────────────── (App)
            Γ ⊢ e1 e2 : τ2

把这条规则直接读成一段 Python 代码：

def synth_app(env, app_expr):
    fn_ty = synth(env, app_expr.fn)
    if not isinstance(fn_ty, Arrow):
        raise TypeError_("application expects function")
    arg_ty = synth(env, app_expr.arg)
    if arg_ty != fn_ty.src:
        raise TypeError_("argument type mismatch")
    return fn_ty.dst

每条规则都可以这样翻译：

前提里出现的 Γ ⊢ ei : τi 翻译成 synth(env, ei) 的调用。
类型约束（如 τ1 → τ2 形式）翻译成 isinstance 与字段相等性判断。
结论的 τ 翻译成函数返回值。

这种"按规则结构对应函数结构"的写法叫 synthesis-directed type checking。如果再加一组 check(env, e, ty) 函数处理"已知期望类型"的情形，就是工业系统常用的双向类型检查。本篇代码只用 synthesis，足够展示骨架。

完整的 STLC 类型检查器

下面是带 →、×、+、Unit、Void 的完整 STLC 类型检查器。

from __future__ import annotations
from dataclasses import dataclass
from typing import Dict, Union


# ---- Types ----
@dataclass(frozen=True)
class TVar:
    name: str
    def __str__(self): return self.name

@dataclass(frozen=True)
class Arrow:
    src: "Type"
    dst: "Type"
    def __str__(self): return f"({self.src} -> {self.dst})"

@dataclass(frozen=True)
class Prod:
    fst: "Type"
    snd: "Type"
    def __str__(self): return f"({self.fst} * {self.snd})"

@dataclass(frozen=True)
class Sum:
    left: "Type"
    right: "Type"
    def __str__(self): return f"({self.left} + {self.right})"

@dataclass(frozen=True)
class UnitT:
    def __str__(self): return "Unit"

@dataclass(frozen=True)
class VoidT:
    def __str__(self): return "Void"

Type = Union[TVar, Arrow, Prod, Sum, UnitT, VoidT]


# ---- Expressions ----
@dataclass(frozen=True)
class Var:
    name: str

@dataclass(frozen=True)
class Lam:
    param: str
    param_ty: Type
    body: "Expr"

@dataclass(frozen=True)
class App:
    fn: "Expr"
    arg: "Expr"

@dataclass(frozen=True)
class Pair:
    fst: "Expr"
    snd: "Expr"

@dataclass(frozen=True)
class Fst:
    expr: "Expr"

@dataclass(frozen=True)
class Snd:
    expr: "Expr"

@dataclass(frozen=True)
class InL:
    expr: "Expr"
    other: Type   # 注入需要标注另一支的类型

@dataclass(frozen=True)
class InR:
    expr: "Expr"
    other: Type

@dataclass(frozen=True)
class Case:
    scrut: "Expr"
    lname: str
    lbody: "Expr"
    rname: str
    rbody: "Expr"

@dataclass(frozen=True)
class TT:
    pass  # ()

@dataclass(frozen=True)
class Absurd:
    expr: "Expr"
    result_ty: Type

Expr = Union[Var, Lam, App, Pair, Fst, Snd, InL, InR, Case, TT, Absurd]


# ---- Type checker ----
class TypeError_(Exception):
    pass


def synth(env: Dict[str, Type], e: Expr) -> Type:
    if isinstance(e, Var):
        if e.name not in env:
            raise TypeError_(f"unbound variable: {e.name}")
        return env[e.name]
    if isinstance(e, Lam):
        new_env = dict(env); new_env[e.param] = e.param_ty
        body_ty = synth(new_env, e.body)
        return Arrow(e.param_ty, body_ty)
    if isinstance(e, App):
        fn_ty = synth(env, e.fn)
        if not isinstance(fn_ty, Arrow):
            raise TypeError_(f"application expects function, got {fn_ty}")
        arg_ty = synth(env, e.arg)
        if arg_ty != fn_ty.src:
            raise TypeError_(f"argument type {arg_ty} != expected {fn_ty.src}")
        return fn_ty.dst
    if isinstance(e, Pair):
        return Prod(synth(env, e.fst), synth(env, e.snd))
    if isinstance(e, Fst):
        t = synth(env, e.expr)
        if not isinstance(t, Prod):
            raise TypeError_(f"fst expects product, got {t}")
        return t.fst
    if isinstance(e, Snd):
        t = synth(env, e.expr)
        if not isinstance(t, Prod):
            raise TypeError_(f"snd expects product, got {t}")
        return t.snd
    if isinstance(e, InL):
        left_ty = synth(env, e.expr)
        return Sum(left_ty, e.other)
    if isinstance(e, InR):
        right_ty = synth(env, e.expr)
        return Sum(e.other, right_ty)
    if isinstance(e, Case):
        s_ty = synth(env, e.scrut)
        if not isinstance(s_ty, Sum):
            raise TypeError_(f"case expects sum, got {s_ty}")
        env_l = dict(env); env_l[e.lname] = s_ty.left
        env_r = dict(env); env_r[e.rname] = s_ty.right
        t1 = synth(env_l, e.lbody)
        t2 = synth(env_r, e.rbody)
        if t1 != t2:
            raise TypeError_(f"case branches differ: {t1} vs {t2}")
        return t1
    if isinstance(e, TT):
        return UnitT()
    if isinstance(e, Absurd):
        t = synth(env, e.expr)
        if not isinstance(t, VoidT):
            raise TypeError_(f"absurd expects Void, got {t}")
        return e.result_ty
    raise TypeError_(f"unknown expression: {e}")

代码风格刻意保守：每条类型规则对应 synth 里一个 isinstance 分支，分支体几乎一行一行对照规则前提，把 BNF 语法树转成类型判断。没有任何"启发式"，没有"猜测"，完全是机械步骤。

注：InL / InR 需要额外标注"另一支的类型"。原因是仅看 inl e 无法推出 τ1 + τ2 里的 τ2 是什么；工业系统通常通过"双向 / 期望类型"传播来避免这个标注，本篇为了保留 synthesis 路径不引入 checking 模式。

跑一遍上一篇的全部定理

把上一篇出现过的所有 STLC 项当成"证明项"喂给类型检查器：

A, B, C = TVar("A"), TVar("B"), TVar("C")

# 1. P -> P
identity = Lam("x", A, Var("x"))
print("id            :", synth({}, identity))

# 2. P -> Q -> P
const_law = Lam("x", A, Lam("y", B, Var("x")))
print("const         :", synth({}, const_law))

# 3. P * Q -> Q * P
pair_swap = Lam("p", Prod(A, B), Pair(Snd(Var("p")), Fst(Var("p"))))
print("pair_swap     :", synth({}, pair_swap))

# 4. (P -> Q -> R) -> (P * Q -> R)
uncurry = Lam("f", Arrow(A, Arrow(B, C)),
              Lam("p", Prod(A, B),
                  App(App(Var("f"), Fst(Var("p"))), Snd(Var("p")))))
print("uncurry       :", synth({}, uncurry))

# 5. (P * Q -> R) -> (P -> Q -> R)
curry = Lam("f", Arrow(Prod(A, B), C),
            Lam("x", A,
                Lam("y", B,
                    App(Var("f"), Pair(Var("x"), Var("y"))))))
print("curry         :", synth({}, curry))

# 6. modus ponens
mp = Lam("p", A, Lam("f", Arrow(A, B), App(Var("f"), Var("p"))))
print("modus_ponens  :", synth({}, mp))

# 7. ¬(P * ¬P)：P * (P -> Void) -> Void
no_contradiction = Lam("p", Prod(A, Arrow(A, VoidT())),
                       App(Snd(Var("p")), Fst(Var("p"))))
print("¬(P × ¬P)     :", synth({}, no_contradiction))

# 8. ex falso：Void -> A
ex_falso = Lam("v", VoidT(), Absurd(Var("v"), A))
print("ex_falso      :", synth({}, ex_falso))

跑这段代码的真实输出：

id            : (A -> A)
const         : (A -> (B -> A))
pair_swap     : ((A * B) -> (B * A))
uncurry       : ((A -> (B -> C)) -> ((A * B) -> C))
curry         : (((A * B) -> C) -> (A -> (B -> C)))
modus_ponens  : (A -> ((A -> B) -> B))
¬(P × ¬P)     : ((A * (A -> Void)) -> Void)
ex_falso      : (Void -> A)

每行输出是一条命题的类型形式，对应 BHK 解释下的"我们刚刚机械地构造了它的证明"。其中：

modus_ponens 的类型是 A → (A → B) → B，对应"假言推理"。
¬(P × ¬P) 的类型是 (A × (A → Void)) → Void，对应"矛盾律"。
ex_falso 的类型是 Void → A，对应"爆炸原理"。

注意：跑通的不是"程序"，而是"证明"。这 8 条 Python 表达式同时是 8 条 STLC 证明项，它们的类型同时是 8 条直觉主义命题逻辑定理。

错误信息也是机械的

故意写两段"错的证明"，看类型检查器怎样定位：

try:
    bad = Lam("x", A, Var("y"))
    synth({}, bad)
except TypeError_ as e:
    print("捕获预期错误:", e)

try:
    # P 类型当函数用：自应用
    bad2 = Lam("p", A, App(Var("p"), Var("p")))
    synth({}, bad2)
except TypeError_ as e:
    print("捕获预期错误:", e)

真实输出：

1 2	`捕获预期错误: unbound variable: y 捕获预期错误: application expects function, got A`

第一条对应"引用了未在上下文里出现的假设"，第二条对应"试图把不是函数的东西当函数用"——分别是逻辑上的"非法引用未声明前提"与"非法应用规则"。错误信息直接由规则约束反推得到，不需要额外的 ad-hoc 检查。

算法终止性

synth 的递归只在 e 的子表达式上发生。STLC 表达式是有限深的语法树，因此递归一定终止。

类型相等性比较（arg_ty != fn_ty.src）在 STLC 里也是结构性的：两个类型 Arrow(A, B) 与 Arrow(A, B) 相等当且仅当子结构对应相等。这种比较走完类型树就停。

在依值类型系统里这一步会变得复杂：类型可能依赖未求值的表达式，需要先归一化再比较。强归一化定理保证这一步在良类型表达式上仍能停。

因此 STLC 的类型检查算法是机械的、可终止的、可被任何编程语言实现的。这条结论在依值类型系统里仍然成立（在前述归一化前提下），是 Lean 4 / Coq / Agda 内核可工程化的核心保证。

与工程语言里的类型检查器对比

工业语言的类型检查器（Java、Rust、TypeScript）做的事情结构上和上面这段 200 行代码相似：

维护类型上下文。
对每种语法结构匹配一组规则。
子表达式调用 synth 或 check，结果汇总成当前节点的类型。
出错时按规则反推错误信息。

差别只在两件事：

类型系统的丰富度。Rust 多了所有权与生命周期，TypeScript 多了结构化子类型，但骨架仍然是上面这一套递归。
类型系统是否能编码定理。Java / Rust / TypeScript 的类型系统不能表达 ∀ x : Nat, P(x) 这种依值命题，因此它们的"编译通过"只保证类型安全，不保证程序符合规约。

真正让"编译通过 = 定理得证"成立的，不是"有类型检查器"这件事本身，而是"类型系统强到能把规约写成类型"。后续 05、06 篇展开的依值类型与归纳类型，就是在 STLC 上补齐这两块表达力。

模式提炼

模式	内容
规则即函数	每条 `Γ ⊢ e : τ` 规则对应类型检查器里一段 `synth` 分支
错误即规则失败	类型错误信息天然由规则前提反推得到，不需要额外脚手架
算法机械可终止	在 STLC 中 synthesis 沿 AST 递归，必停
工业类型检查同形	Java / Rust / TS 的类型检查器骨架与本文一致，差别在丰富度与表达力
类型够强才证定理	类型检查器的"编译通过"语义强度由类型系统的表达力决定

给读者的练习

给上面的检查器加一条"同步类型"规则：当 App 的参数表达式类型与函数源类型不一致时，输出更具体的错误（指出哪个参数、期望什么、得到什么）。
把 InL / InR 改成双向检查（check(env, e, ty)），消除"必须标注另一支类型"的额外参数。
给检查器加上 let x = e1 in e2 语法糖：把它翻译成 (λ x : τ. e2) e1 后复用现有规则。
拓展：尝试加一条"有限 Nat 与 succ / zero"，会发现 STLC 写不出递归。回想上一篇为什么递归被故意拿掉。

衔接到下一篇

至此，"类型检查 = 证明检查"已经从概念落到一段可运行的程序。但 STLC 太小，只能编码命题逻辑，写不出"对任意自然数 n，n + 0 = n"这种带量词的命题。

下一篇引入依值类型：允许类型依赖表达式，把 ∀ 翻译成依值函数类型 Π x : A. B(x)，把 ∃ 翻译成依值积类型 Σ x : A. B(x)。从这一步开始，类型系统第一次能直接表达"对所有的"和"存在某个"。

参考资料

Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002（第 9、11 章）.
David Raymond Christiansen. Bidirectional Typing Rules: A Tutorial. 2013.
Jana Dunfield, Neel Krishnaswami. Bidirectional Typing. ACM Computing Surveys, 2021.
Robert Harper. Practical Foundations for Programming Languages. Cambridge, 2016.