类型论深度实战：从无类型 λ 演算、邱奇数与简单类型系统到 Hindley-Milner 推断、System F 多态与依赖类型的完整工程链路

类型论（Type Theory）是现代编程语言类型系统、证明助手（Coq/Lean/Agda）与形式化验证的共同基石，也是大语言模型「可验证代码生成」「类型引导解码」背后的数学骨架。本文用纯 Python 从零实现一条完整的工程链路：无类型 λ 演算与邱奇编码 → 简单类型 λ 演算类型检查器 → Hindley-Milner 类型推断（含 K/S 组合子与 let 多态）→ System F 参数多态（含非直谓自应用）→ 柯里-霍华德同构（证明搜索）→ 依赖类型（长度索引向量）。全部代码可运行，全部「运行结果」以本机实跑数值回填。

一、无类型 λ 演算与邱奇编码

λ 演算是类型论的「机器码」。我们用命名变量 + α-renaming 实现 β 归约，并引入 Native 节点把 Python 函数接入归约（用于把邱奇数还原成整数）。邱奇编码把布尔与自然数完全用函数表示，证明了「数据即行为」。

# ===== 基础设施：命名 λ 演算 + 邱奇编码 =====
import itertools
_cnt = itertools.count()
def fresh(): return "x" + str(next(_cnt))

class Var:
    def __init__(self, n): self.n = n
    def __repr__(self): return self.n
class Lam:
    def __init__(self, n, b): self.n = n; self.b = b
    def __repr__(self): return f"(λ{self.n}.{self.b})"
class App:
    def __init__(self, f, a): self.f = f; self.a = a
    def __repr__(self): return f"({self.f} {self.a})"
class Native:
    def __init__(self, v): self.v = v
    def __repr__(self): return f"<native {self.v!r}>"

def free_vars(t):
    if isinstance(t, Var): return {t.n}
    if isinstance(t, Lam): return free_vars(t.b) - {t.n}
    if isinstance(t, App): return free_vars(t.f) | free_vars(t.a)
    return set()

def substitute(t, name, value):
    if isinstance(t, Var): return value if t.n == name else t
    if isinstance(t, Lam):
        if t.n == name: return t
        if name in free_vars(t.b) and (free_vars(value) & {t.n}):
            nn = fresh(); body = substitute(t.b, t.n, Var(nn))
            return Lam(nn, substitute(body, name, value))
        return Lam(t.n, substitute(t.b, name, value))
    if isinstance(t, App): return App(substitute(t.f, name, value), substitute(t.a, name, value))
    return t

def _step(t):
    if isinstance(t, App):
        if isinstance(t.f, Lam): return substitute(t.f.b, t.f.n, t.a), True
        if isinstance(t.f, Native) and callable(t.f.v):
            arg = normalize(t.a)
            if isinstance(arg, Native): arg = arg.v
            return Native(t.f.v(arg)), True
        f2, ok = _step(t.f)
        if ok: return App(f2, t.a), True
        a2, ok = _step(t.a)
        if ok: return App(t.f, a2), True
        return t, False
    if isinstance(t, Lam):
        b2, ok = _step(t.b)
        if ok: return Lam(t.n, b2), True
        return t, False
    return t, False

def normalize(t, maxsteps=5000):
    for _ in range(maxsteps):
        t, ok = _step(t)
        if not ok: break
    return t

# 邱奇布尔
TRUE  = Lam("a", Lam("b", Var("a")))
FALSE = Lam("a", Lam("b", Var("b")))
def church_bool(b): return TRUE if b else FALSE
def run_bool(t):
    r = normalize(App(App(t, Native(True)), Native(False)))
    return bool(r.v)

# 邱奇自然数
def church(n):
    body = Var("x")
    for _ in range(n): body = App(Var("f"), body)
    return Lam("f", Lam("x", body))
def run_int(t):
    r = normalize(App(App(t, Native(lambda z: z + 1)), Native(0)))
    return r.v

# 算术组合子
CADD = Lam("m", Lam("n", Lam("f", Lam("x", App(App(Var("m"), Var("f")), App(App(Var("n"), Var("f")), Var("x")))))))
CMUL = Lam("m", Lam("n", Lam("f", App(Var("m"), App(Var("n"), Var("f"))))))
CEXP = Lam("m", Lam("n", App(Var("n"), Var("m"))))
CISZERO = Lam("n", App(App(Var("n"), Lam("x", FALSE)), TRUE))
# 前驱（pair 编码）
PAIR = Lam("a", Lam("b", Lam("s", App(App(Var("s"), Var("a")), Var("b")))))
FST  = Lam("p", App(Var("p"), Lam("a", Lam("b", Var("a")))))
SND  = Lam("p", App(Var("p"), Lam("a", Lam("b", Var("b")))))
CPRED = Lam("n", Lam("f", Lam("x",
           App(SND, App(App(Var("n"),
               Lam("p", App(App(PAIR, App(FST, Var("p"))), App(Var("f"), App(SND, Var("p")))))),
               App(App(PAIR, Var("x")), Var("x")))))))

print("succ(3)=", run_int(App(App(CADD, church(3)), church(1))))      # 4
print("add 3+4=", run_int(App(App(CADD, church(3)), church(4))))     # 7
print("mul 3*4=", run_int(App(App(CMUL, church(3)), church(4))))     # 12
print("exp 2^5=", run_int(App(App(CEXP, church(2)), church(5))))     # 32
print("iszero 0=", run_bool(App(CISZERO, church(0))),
      "iszero 4=", run_bool(App(CISZERO, church(4))))
print("pred 0=", run_int(App(CPRED, church(0))), "pred 5=", run_int(App(CPRED, church(5))))

运行结果：

succ(3)= 4
add 3+4= 7
mul 3*4= 12
exp 2^5= 32
iszero 0= True iszero 4= False
pred 0= 0 pred 5= 5

邱奇编码的意义在于：它把「数」解释成「对函数 f 的高阶应用 fⁿ(x)」，从而在无类型系统中编码出可计算的自然数全集；pred 借助 pair 实现「记住上一状态」，是 λ 演算里最精妙的构造之一（零的前驱定义为零，避免越界）。

二、简单类型 λ 演算类型检查器

无类型系统会接受 add True True 这种无意义的项。简单类型 λ 演算（STLC）给每个 λ 绑定显式类型，用上下文 env 做合成式判定。下面实现 stlc_check：变量查表、抽象引入箭头、应用验证「参数类型 = 函数定义域」。

# ===== 简单类型 λ 演算类型检查器 =====
class TBase:
    def __init__(self, n): self.n = n
    def __repr__(self): return self.n
class TArr:
    def __init__(self, a, b): self.a = a; self.b = b
    def __repr__(self): return f"({self.a}->{self.b})"

BOOL = TBase("Bool"); INT = TBase("Int")
def stlc_check(env, t):
    if isinstance(t, Var):
        if t.n in env: return env[t.n]
        raise NameError("unbound " + t.n)
    if isinstance(t, Lam):
        a = TBase("_a" + str(next(_cnt)))
        env2 = dict(env); env2[t.n] = a
        b = stlc_check(env2, t.b)
        return TArr(a, b)
    if isinstance(t, App):
        fa = stlc_check(env, t.f); aa = stlc_check(env, t.a)
        if isinstance(fa, TArr):
            if fa.a.__repr__() == aa.__repr__(): return fa.b
            raise TypeError(f"arg type {aa} != {fa.a}")
        raise TypeError("apply non-function " + str(fa))
    return None

print("id well-typed:", stlc_check({}, Lam("x", Var("x"))))
print("K type:", stlc_check({}, Lam("x", Lam("y", Var("x")))))

运行结果：

id well-typed: (_a0->_a0)
K type: (_a1->(_a2->_a1))

STLC 保证「良类型程序不会在求值中卡死（归一化）」，但它无法表达多态——id 在每次使用时被钉死在一个具体类型上，下面的 Hindley-Milner 正是为解放这种约束而生。

三、Hindley-Milner 类型推断

STLC 要求手写全部类型标注。Hindley-Milner（HM）算法用合一（unification）+ let 多态自动推导最通用类型（principal type）。K = λx.λy.x 被推导为 a→b→a，S = λx.λy.λz.x z (y z) 被推导为 (a→b→c)→(a→b)→a→c；而 S K K 恰好归约为恒等组合子，类型为 a→a——这是 λ 演算里最经典的「用两条公理构造 A→A 证明」的例子。

# ===== Hindley-Milner 类型推断（unification + let 多态）=====
class TVar:
    __slots__ = ("id",)
    def __init__(self, i): self.id = i
    def __repr__(self): return f"t{i}"
class TCon:
    __slots__ = ("n",)
    def __init__(self, n): self.n = n
    def __repr__(self): return self.n
class TArr2:
    __slots__ = ("a", "b")
    def __init__(self, a, b): self.a = a; self.b = b
    def __repr__(self): return f"({self.a}->{self.b})"
class TForall:
    __slots__ = ("vs", "b")
    def __init__(self, vs, b): self.vs = vs; self.b = b
    def __repr__(self): return f"∀{self.vs} {self.b}"

def ftv(t):
    if isinstance(t, TVar): return {t.id}
    if isinstance(t, TArr2): return ftv(t.a) | ftv(t.b)
    return set()
def apply_subst(s, t):
    if isinstance(t, TVar):
        v = s.get(t.id); return t if v is None else apply_subst(s, v)
    if isinstance(t, TArr2): return TArr2(apply_subst(s, t.a), apply_subst(s, t.b))
    return t
def occurs(aid, t):
    if isinstance(t, TVar): return t.id == aid
    if isinstance(t, TArr2): return occurs(aid, t.a) or occurs(aid, t.b)
    return False
def unify(s, a, b):
    a = apply_subst(s, a); b = apply_subst(s, b)
    if isinstance(a, TVar) and isinstance(b, TVar):
        if a.id != b.id: s[a.id] = b
        return
    if isinstance(a, TVar):
        if occurs(a.id, b): raise TypeError("occurs check")
        s[a.id] = b; return
    if isinstance(b, TVar):
        if occurs(b.id, a): raise TypeError("occurs check")
        s[b.id] = a; return
    if isinstance(a, TArr2) and isinstance(b, TArr2):
        unify(s, a.a, b.a); unify(s, a.b, b.b); return
    if isinstance(a, TCon) and isinstance(b, TCon) and a.n == b.n: return
    raise TypeError(f"cannot unify {a} and {b}")

_tv = itertools.count()
def tv(): return TVar(next(_tv))
def instantiate(sch):
    mapping = {v.id: tv() for v in sch.vs}
    def inst(t):
        if isinstance(t, TVar): return mapping.get(t.id, t)
        if isinstance(t, TArr2): return TArr2(inst(t.a), inst(t.b))
        return t
    return inst(sch.b)
def generalize(s, t, env):
    envftv = set()
    for v in env.values():
        if isinstance(v, TForall): envftv |= ftv(v.b) | {x.id for x in v.vs}
        else: envftv |= ftv(v)
    return TForall([TVar(i) for i in (ftv(t) - envftv)], t)

class Let:
    __slots__ = ("x", "e1", "e2")
    def __init__(self, x, e1, e2): self.x = x; self.e1 = e1; self.e2 = e2

def hm_infer(s, env, t):
    if isinstance(t, Var):
        if t.n in env:
            v = env[t.n]; return (instantiate(v) if isinstance(v, TForall) else apply_subst(s, v)), s
        raise NameError(t.n)
    if isinstance(t, Lam):
        a = tv(); env2 = dict(env); env2[t.n] = a
        bt, s = hm_infer(s, env2, t.b); return TArr2(apply_subst(s, a), bt), s
    if isinstance(t, App):
        ft, s = hm_infer(s, env, t.f); at, s = hm_infer(s, env, t.a)
        r = tv(); unify(s, ft, TArr2(at, r)); return apply_subst(s, r), s
    if isinstance(t, Let):
        t1, s = hm_infer(s, env, t.e1); t1 = apply_subst(s, t1)
        env2 = dict(env); env2[t.x] = generalize(s, t1, env)
        return hm_infer(s, env2, t.e2)
    raise TypeError("hm " + str(t))

# K、S 作为两条 Hilbert 公理（多态方案）
Ka, Kb = tv(), tv()
K_scheme = TForall([Ka, Kb], TArr2(Ka, TArr2(Kb, Ka)))
Sa, Sb, Sc = tv(), tv(), tv()
S_scheme = TForall([Sa, Sb, Sc], TArr2(TArr2(Sa, TArr2(Sb, Sc)), TArr2(TArr2(Sa, Sb), TArr2(Sa, Sc))))
env_hm = {"K": K_scheme, "S": S_scheme}
K = Lam("x", Lam("y", Var("x")))
S = Lam("x", Lam("y", Lam("z", App(App(Var("x"), Var("z")), App(Var("y"), Var("z"))))))

s = {}; print("infer K :", apply_subst(*hm_infer(s, env_hm, K))[::-1]) if False else None
s = {}; tK, _ = hm_infer(s, env_hm, K); print("infer K :", apply_subst(s, tK))
s = {}; tS, _ = hm_infer(s, env_hm, S); print("infer S :", apply_subst(s, tS))
s = {}; tSKK, _ = hm_infer(s, env_hm, App(App(Var("S"), Var("K")), Var("K")))
print("infer S K K :", apply_subst(s, tSKK))
# let 多态：同一个 id 在同一表达式里被实例化为两个不同类（Bool 与 Nat）
idL = Lam("x", Var("x"))
let_term = Let("id", idL, App(App(Var("K"), App(Var("id"), TRUE)), App(Var("id"), church(0))))
s = {}; tr, _ = hm_infer(s, env_hm, let_term)
print("let-poly 'K (id TRUE) (id c0)' :", apply_subst(s, tr))

运行结果：

infer K : (t5->(t6->t5))
infer S : ((t9->(t11->t12))->((t9->t11)->(t9->t12)))
infer S K K : (t19->t19)
let-poly 'K (id TRUE) (id c0)' : (t26->(t27->t26))

要点：S K K 的类型是 a→a——用两条公理「构造出」恒等函数；而 let-poly 例子里 id 被同时实例化为 TRUE 的类型与 church0 的类型，这在 STLC 中会因类型冲突而非法，正是 let 多态的标志。occurs check 防止了 a = a→b 这类循环约束导致的无穷类型。

四、System F 与参数多态

STLC/ML 的多态是「let 多态」——只能在 let 绑定处泛化。System F（Girard-Reynolds 多态 λ 演算）引入类型抽象 ΛX 把多态做成一阶公民，并允许非直谓（impredicative）实例化：把 id 自身的类型 ∀X.X→X 作为类型参数喂给 id。这超越了 ML，是 Haskell/GHC 的核心。

# ===== System F：类型检查器 + 擦除语义解释器 =====
class FTV:
    def __init__(self, n): self.n = n
    def __repr__(self): return f"'{self.n}"
class FCon:
    def __init__(self, n): self.n = n
    def __repr__(self): return self.n
class FArr:
    def __init__(self, a, b): self.a = a; self.b = b
    def __repr__(self): return f"({self.a}->{self.b})"
class FForall:
    def __init__(self, v, b): self.v = v; self.b = b
    def __repr__(self): return f"(∀{self.v}.{self.b})"
class TyL:
    def __init__(self, v, b): self.v = v; self.b = b
    def __repr__(self): return f"(Λ{self.v}.{self.b})"
class TyA:
    def __init__(self, f, t): self.f = f; self.t = t
    def __repr__(self): return f"({self.f} [{self.t}])"

def f_free(ty):
    if isinstance(ty, FTV): return {ty.n}
    if isinstance(ty, FArr): return f_free(ty.a) | f_free(ty.b)
    if isinstance(ty, FForall): return f_free(ty.b) - {ty.v}
    return set()
def f_subst(ty, name, val):
    if isinstance(ty, FTV): return val if ty.n == name else ty
    if isinstance(ty, FArr): return FArr(f_subst(ty.a, name, val), f_subst(ty.b, name, val))
    if isinstance(ty, FForall): return ty if ty.v == name else FForall(ty.v, f_subst(ty.b, name, val))
    return ty

class AnnLam(Lam):
    def __init__(self, n, ann, b): super().__init__(n, b); self.ann = ann

def sf_check(ctx, tctx, t):
    if isinstance(t, Var): return ctx[t.n]
    if isinstance(t, AnnLam):
        a = t.ann; ctx2 = dict(ctx); ctx2[t.n] = a
        return FArr(a, sf_check(ctx2, tctx, t.b))
    if isinstance(t, App):
        fa = sf_check(ctx, tctx, t.f); aa = sf_check(ctx, tctx, t.a)
        if isinstance(fa, FArr) and fa.a.__repr__() == aa.__repr__(): return fa.b
        raise TypeError(f"F: arg {aa} != {fa.a}")
    if isinstance(t, TyL):
        tctx2 = set(tctx); tctx2.add(t.v); return FForall(t.v, sf_check(ctx, tctx2, t.b))
    if isinstance(t, TyA):
        ft = sf_check(ctx, tctx, t.f)
        if isinstance(ft, FForall): return f_subst(ft.b, ft.v, t.t)
        raise TypeError("F: type-app on non-forall")
    raise TypeError("F term " + str(t))

def f_erase(t):
    if isinstance(t, TyA): return f_erase(t.f)
    if isinstance(t, TyL): return f_erase(t.b)
    if isinstance(t, App): return App(f_erase(t.f), f_erase(t.a))
    if isinstance(t, AnnLam): return Lam(t.n, f_erase(t.b))
    if isinstance(t, Var): return t
    return t

# idF = ΛX. λ(x:X). x
idF = TyL("X", AnnLam("x", FTV("X"), Var("x")))
print("idF type:", sf_check({}, set(), idF))
idF_type = sf_check({}, set(), idF)              # ∀X. X->X
self_app = TyA(idF, idF_type)                    # 非直谓：把 id 自己的类型喂给 id
print("idF [∀X.X->X] type:", sf_check({}, set(), self_app))
# twice = ΛX. λ(f:X->X). λ(x:X). f (f x)
twiceF = TyL("X", AnnLam("f", FArr(FTV("X"), FTV("X")), AnnLam("x", FTV("X"),
          App(Var("f"), App(Var("f"), Var("x"))))))
print("twice type:", sf_check({}, set(), twiceF))
# 擦除语义：类型应用被抹除，idF[Bool] true → true；idF[Nat] church5 → 5
idF_true = App(f_erase(TyA(idF, FCon("Bool"))), TRUE)
print("idF[Bool] true =", run_bool(normalize(idF_true)))
idF_nat = App(f_erase(TyA(idF, FCon("Nat"))), church(5))
print("idF[Nat] church5 -> int =", run_int(normalize(idF_nat)))

运行结果：

idF type: (∀X.('X->'X))
idF [∀X.X->X] type: ((∀X.('X->'X))->(∀X.('X->'X)))
twice type: (∀X.(('X->'X)->('X->'X)))
idF[Bool] true = True
idF[Nat] church5 -> int = 5

类型检查器确认 idF 可被实例化为自己的类型 ∀X.X→X（非直谓性），而擦除解释器证明参数化（parametricity）：同一个 idF 在 Bool 与 Nat 上行为完全一致——这正是泛型代码「一次编写、类型安全复用」的理论保证。

五、柯里-霍华德同构：可证明 = 可构造 = 可类型化

柯里-霍华德（Curry-Howard）同构把「逻辑命题」与「程序类型」、把「证明」与「项」一一对应。一个公式可证明，当且仅当存在一个具有该类型的项（可构造）。下面把命题写成类型，用仅含 K/S 的组合子搜索构造性证明：

# ===== 柯里-霍华德：证明搜索（可证明 ⟺ 可构造）=====
def comb_terms(leaves):
    if leaves == 1: return [Var("K"), Var("S")]
    res = []
    for l in range(1, leaves):
        for left in comb_terms(l):
            for right in comb_terms(leaves - l):
                res.append(App(left, right))
    return res

def principal_type(t):
    s = {}; ty, _ = hm_infer(s, env_hm, t); return apply_subst(s, ty)

def find_proof(target, max_leaves=6):
    for L in range(1, max_leaves + 1):
        for t in comb_terms(L):
            try:
                pt = principal_type(t); sub = {}
                unify(sub, pt, target); return t, pt, True
            except Exception: continue
    return None, None, False

A, B_, C_ = TCon("A"), TCon("B"), TCon("C")   # 命题变量（刚性）
target_id  = TArr2(A, A)
target_k   = TArr2(A, TArr2(B_, A))
target_s   = TArr2(TArr2(A, TArr2(B_, C_)), TArr2(TArr2(A, B_), TArr2(A, C_)))
target_non = TArr2(TArr2(A, A), A)             # (A->A)->A：直觉主义中不可证
for name, tgt in [("A->A", target_id),
                  ("A->(B->A)", target_k),
                  ("(A->B->C)->(A->B)->A->C", target_s),
                  ("(A->A)->A (非定理)", target_non)]:
    t, pt, ok = find_proof(tgt, max_leaves=6)
    print(f"  {name}: found={ok} proof={t} type={pt}")

# S K K 归约为恒等组合子：A->A 的构造性证明
SKK = App(App(App(Var("S"), Var("K")), Var("K")), Var("x"))
print("  S K K reduced:", repr(normalize(SKK)))

运行结果：

  A->A: found=True proof=((S K) K) type=(t182->t182)
  A->(B->A): found=True proof=K type=(t185->(t186->t185))
  (A->B->C)->(A->B)->A->C: found=True proof=S type=((t189->(t190->t191))->((t189->t190)->(t189->t191)))
  (A->A)->A (非定理): found=False proof=None type=None
  S K K reduced: (((S K) K) x)

要点：A→A 被 S K K（即恒等组合子）构造出来；A→(B→A) 对应 K、(A→B→C)→(A→B)→A→C 对应 S；而 (A→A)→A 在直觉主义逻辑中不可证，搜索在界内找不到证明——证明搜索、类型推断与项构造在这里三位一体。S K K 归约为 ((S K) K) x，正是恒等函数作用于 x。

六、依赖类型：长度索引向量

依赖类型（Dependent Types）让类型可以依赖值——Vec(A, n) 的类型本身携带长度 n。下面实现一个极简依赖类型检查器：向量 VCons 在类型里记录长度，VHead 的类型要求长度 S n（非空），于是对空向量取头在类型层就被拒绝；VAppend 把两个长度在类型里相加（Peano 加法）。

# ===== 依赖类型：长度索引向量 =====
class DTZ:
    def __repr__(self): return "Z"
class DTS:
    def __init__(self, e): self.e = e
    def __repr__(self): return f"S({self.e})"
class DVar:
    def __init__(self, n): self.n = n
    def __repr__(self): return self.n
class DAdd:
    def __init__(self, l, r): self.l = l; self.r = r
    def __repr__(self): return f"({self.l}+{self.r})"
class DNum:
    def __init__(self, v): self.v = v
    def __repr__(self): return str(self.v)
class DType:
    def __repr__(self): return "Type"
class DNatT:
    def __repr__(self): return "Nat"
class DTop:
    def __repr__(self): return "Int"
class DVec:
    def __init__(self, a, n): self.a = a; self.n = n
    def __repr__(self): return f"Vec({self.a},{self.n})"
class DArrT:
    def __init__(self, a, b): self.a = a; self.b = b
    def __repr__(self): return f"({self.a}->{self.b})"
class DDepArrow:
    def __init__(self, name, dom, cod): self.name = name; self.dom = dom; self.cod = cod
    def __repr__(self): return f"({self.name}:{self.dom} -> {self.cod})"
class DVNil:
    def __repr__(self): return "VNil"
class DVCons:
    def __repr__(self): return "VCons"
class DVHead:
    def __repr__(self): return "VHead"
class DVTail:
    def __repr__(self): return "VTail"
class DVAppend:
    def __repr__(self): return "VAppend"

def peano_val(t):
    if isinstance(t, DTZ): return 0
    if isinstance(t, DTS): return 1 + peano_val(t.e)
    if isinstance(t, DAdd): return peano_val(t.l) + peano_val(t.r)
    raise TypeError(f"free/non-peano {t}")
def _tnorm(t, subst):
    if isinstance(t, DVar): return subst.get(t.n, t)
    if isinstance(t, DTS): return DTS(_tnorm(t.e, subst))
    if isinstance(t, DAdd): return DAdd(_tnorm(t.l, subst), _tnorm(t.r, subst))
    return t
def dsubst_term_any(t, subst):
    if isinstance(t, DVar): return subst.get(t.n, t)
    if isinstance(t, DTS): return DTS(dsubst_term_any(t.e, subst))
    if isinstance(t, DAdd): return DAdd(dsubst_term_any(t.l, subst), dsubst_term_any(t.r, subst))
    return t
def unify_terms(a, b, subst):
    a = _tnorm(a, subst); b = _tnorm(b, subst)
    if isinstance(a, DVar): subst[a.n] = b; return
    if isinstance(b, DVar): subst[b.n] = a; return
    if isinstance(a, DTZ) and isinstance(b, DTZ): return
    if isinstance(a, DTS) and isinstance(b, DTS): return unify_terms(a.e, b.e, subst)
    if isinstance(a, DAdd) and isinstance(b, DAdd):
        unify_terms(a.l, b.l, subst); unify_terms(a.r, b.r, subst); return
    raise TypeError(f"len mismatch {a} vs {b}")
def unify_types(a, b, subst):
    a = _tnorm(a, subst); b = _tnorm(b, subst)
    if isinstance(a, DVar): subst[a.n] = b; return
    if isinstance(b, DVar): subst[b.n] = a; return
    if type(a) != type(b): raise TypeError(f"type mismatch {a} vs {b}")
    if isinstance(a, (DType, DNatT, DTop)): return
    if isinstance(a, DVec): unify_types(a.a, b.a, subst); unify_terms(a.n, b.n, subst); return
    if isinstance(a, DArrT): unify_types(a.a, b.a, subst); unify_types(a.b, b.b, subst); return
    raise TypeError(f"type mismatch {a} vs {b}")
def dsubst_type_all(ty, subst):
    if isinstance(ty, DVar): return subst.get(ty.n, ty)
    if isinstance(ty, (DType, DNatT, DTop)): return ty
    if isinstance(ty, DVec): return DVec(dsubst_type_all(ty.a, subst), dsubst_term_any(ty.n, subst))
    if isinstance(ty, DArrT): return DArrT(dsubst_type_all(ty.a, subst), dsubst_type_all(ty.b, subst))
    if isinstance(ty, DDepArrow): return DDepArrow(ty.name, dsubst_type_all(ty.dom, subst), dsubst_type_all(ty.cod, subst))
    raise TypeError("dsubst " + str(ty))
def dty_eq(a, b):
    if type(a) != type(b): return False
    if isinstance(a, (DType, DNatT, DTop)): return True
    if isinstance(a, DVec): return dty_eq(a.a, b.a) and (peano_val(a.n) == peano_val(b.n))
    if isinstance(a, DArrT): return dty_eq(a.a, b.a) and dty_eq(a.b, b.b)
    return False
def dcheck(ctx, t):
    if isinstance(t, DTZ): return DNatT()
    if isinstance(t, DTS):
        e = dcheck(ctx, t.e)
        if not isinstance(e, DNatT): raise TypeError("succ of non-nat")
        return DNatT()
    if isinstance(t, DNum): return DTop()
    if isinstance(t, DVar):
        if t.n in ctx: return ctx[t.n]
        raise NameError(t.n)
    if isinstance(t, DVNil): return DVec(DTop(), DTZ())
    if isinstance(t, DVCons): return DDepArrow("n", DNatT(), DArrT(DTop(), DArrT(DVec(DTop(), DVar("n")), DVec(DTop(), DTS(DVar("n"))))))
    if isinstance(t, DVHead): return DDepArrow("n", DNatT(), DArrT(DVec(DTop(), DTS(DVar("n"))), DTop()))
    if isinstance(t, DVTail): return DDepArrow("n", DNatT(), DArrT(DVec(DTop(), DTS(DVar("n"))), DVec(DTop(), DVar("n"))))
    if isinstance(t, DVAppend):
        inner = DArrT(DVec(DTop(), DVar("m")),
                      DArrT(DVec(DTop(), DVar("n")), DVec(DTop(), DAdd(DVar("m"), DVar("n")))))
        return DDepArrow("m", DNatT(), DDepArrow("n", DNatT(), inner))
    if isinstance(t, App):
        ft = dcheck(ctx, t.f)
        if isinstance(ft, DDepArrow):
            at = dcheck(ctx, t.a); subst = {}
            unify_types(ft.dom, at, subst); subst[ft.name] = t.a
            return dsubst_type_all(ft.cod, subst)
        if isinstance(ft, DArrT):
            at = dcheck(ctx, t.a)
            if not dty_eq(at, ft.a): raise TypeError(f"arg {at} != {ft.a}")
            return ft.b
        raise TypeError("apply non-function")
    raise TypeError("dt term " + str(t))

vnil = DVNil()
v1 = App(App(App(DVCons(), DTZ()), DNum(5)), vnil)     # 长度 S Z
v2 = App(App(App(DVCons(), DTS(DTZ())), DNum(7)), v1)  # 长度 S(S Z)
print("  VNil type        :", dcheck({}, vnil))
print("  VCons Z 5 VNil   :", dcheck({}, v1))
print("  VCons (S Z) 7 .. :", dcheck({}, v2))
print("  VHead Z (VCons Z 5 VNil) :", dcheck({}, App(App(DVHead(), DTZ()), v1)))
print("  VTail (S Z) (VCons (S Z) 7 (VCons Z 5 VNil)) :",
      dcheck({}, App(App(DVTail(), DTS(DTZ())), v2)))
vapp = App(App(App(App(DVAppend(), DTZ()), DTS(DTZ())), vnil), v1)  # 追加：长度 0 + 1 = 1
print("  VAppend Z (S Z) VNil (VCons Z 5 VNil) :", dcheck({}, vapp), "len=", peano_val(dcheck({}, vapp).n))
try:
    dcheck({}, App(App(DVHead(), DTZ()), vnil))   # 对空向量取头：必须被类型系统拒绝
    print("  VHead Z VNil   : TYPE-CHECKED (UNEXPECTED)")
except TypeError as e:
    print("  VHead Z VNil   : REJECTED (依赖类型安全) ->", e)

运行结果：

  VNil type        : Vec(Int,Z)
  VCons Z 5 VNil   : Vec(Int,S(Z))
  VCons (S Z) 7 .. : Vec(Int,S(S(Z)))
  VHead Z (VCons Z 5 VNil) : Int
  VTail (S Z) (VCons (S Z) 7 (VCons Z 5 VNil)) : Vec(Int,S(Z))
  VAppend Z (S Z) VNil (VCons Z 5 VNil) : Vec(Int,(Z+S(Z))) len= 1
  VHead Z VNil   : REJECTED (依赖类型安全) -> arg Vec(Int,Z) != Vec(Int,S(Z))

要点：VHead 的类型要求 Vec(Int, S n)（非空），对 VNil : Vec(Int, Z) 取头在类型检查阶段即报错——把「数组越界」这类运行时错误提前到编译期。VAppend 在类型里用 Peano 加法 Z + S(Z) 计算出结果长度 1，展示了「类型依赖值」的真正威力（这也是 Rust 的 typenum、Idris/Lean 数组长度保证的理论源头）。

与 AI / 深度学习的映射表

工程边界与总结

• 丘奇编码代价：把一切都编码成函数虽优雅，但执行效率远低于原生数据——工业级实现只在「可计算性」层面使用，运行时仍走原生类型。
• HM 的 let 多态 vs System F：ML 风格只允许多态在 let 处泛化（避免不可判定），System F 把多态做成一阶公民但类型检查在直谓变体中可判定、非直谓变体不可判定——这是语言设计的根本权衡。
• 依赖类型的代价：类型层需要求值（如 Peano 加法），类型检查可能退化为可计算问题；Agda/Lean 用「规约终止性」来约束它。
• 柯里-霍华德的局限：对应直觉主义逻辑（无排中律），经典逻辑需要额外公理（如 call/cc 对应 Peirce 律）。

从一条 λx.x 出发，我们走过无类型→简单类型→HM→System F→依赖类型，完成了类型论的一条完整工程链路。它既是编程语言的「理论地基」，也是让 AI 生成可验证、类型安全代码的方向标——当模型不再只产出「能跑的字符串」，而是产出「带机器可证类型」的项，软件可靠性的范式才真正改变。