第3章：简单类型 lambda 演算（最基本的类型系统）The Simply Typed Lambda Calculus — The Most Basic Type System

一、导读

1.1 学习目标

本章探讨简单类型 lambda 演算（Simply Typed Lambda Calculus, STLC），这是最基础也是最核心的类型系统。通过本章的学习，读者将达成以下目标：

• 掌握简单类型的语法定义和类型判断规则
• 理解类型化 lambda 项与无类型 lambda 项的区别
• 熟练掌握类型推导算法和类型检查过程
• 理解强规范化定理及其证明思路
• 认识 STLC 的表达能力限制以及 Curry-Howard 同构在 STLC 中的体现
• 了解 Church 风格与 Curry 风格类型化方法的区别

1.2 重要性

简单类型 lambda 演算是所有类型系统研究的起点。它通过在无类型 lambda 演算中引入类型注解和类型检查规则，获得了类型安全的保证。STLC 虽然简单，但包含了类型系统的所有核心概念：类型环境、类型判断、替换引理、规范化性质等。

STLC 的重要性还体现在它与直觉主义命题逻辑的精确对应（Curry-Howard 同构的最简单形式）。在 STLC 中，类型对应命题，程序对应证明，类型化程序的存在性等价于对应命题的可证明性。这意味着 STLC 不仅是一个编程模型，还是一个逻辑系统。

1.3 核心问题

• 引入类型系统后，哪些无类型 lambda 项变得不合法了？我们失去了什么？
• 为什么所有有类型的 STLC 项都能保证终止？这与无类型 lambda 演算有什么本质区别？
• 类型推导是如何工作的？编译器怎样在不标注类型的情况下确定表达式的类型？
• STLC 对应什么样的逻辑系统？这个对应关系的精确含义是什么？

二、核心概念详解

2.1 简单类型的语法

简单类型（Simple Types）由以下语法递归定义：

T ::= o          -- 基本类型（base type）
    | T → T      -- 箭头类型（函数类型）

其中 o 代表基本类型（如 Bool、Nat 等），箭头类型 T1 → T2 表示从类型 T1 到类型 T2 的函数类型。箭头是右结合的，所以 A → B → C 表示 A → (B → C)。

类型化 lambda 项的语法为：

e ::= x                    -- 变量
    | λx:T. e              -- 类型化抽象（带类型注解的函数定义）
    | e e                  -- 应用

注意与无类型 lambda 演算的关键区别：每个 lambda 抽象都必须标注参数的类型。这个看似简单的约束带来了根本性的变化——它排除了 (λx.x x) 这样的自应用项，因为 x 不能同时具有类型 T 和类型 T → T'。

2.2 类型判断规则

类型判断的形式为 Γ ⊢ e : T，读作"在类型环境 Γ 下，表达式 e 具有类型 T"。类型环境 Γ 是从变量到类型的有限映射，如 {x: Nat, y: Bool}。

三条基本类型判断规则：

变量规则（T-Var）：

Γ(x) = T
-----------
Γ ⊢ x : T

如果类型环境 Γ 将变量 x 映射到类型 T，则 x 在 Γ 下具有类型 T。

抽象规则（T-Abs）：

Γ, x:T1 ⊢ e : T2
-------------------------
Γ ⊢ (λx:T1. e) : T1 → T2

如果在假设 x 具有类型 T1 的前提下，e 具有类型 T2，则 λx:T1.e 具有类型 T1 → T2。

应用规则（T-App）：

Γ ⊢ e1 : T1 → T2    Γ ⊢ e2 : T1
----------------------------------
Γ ⊢ e1 e2 : T2

如果 e1 具有函数类型 T1 → T2，e2 具有类型 T1，则应用 e1 e2 具有类型 T2。

这些规则是语法导向的（syntax-directed），可以算法化地实现为类型检查器。

2.3 类型安全性质

STLC 的类型安全由两个核心定理保证：

进步定理（Progress）：如果 ∅ ⊢ e : T，则 e 要么是一个值（lambda 抽象），要么存在 e' 使得 e → e'。即良类型的表达式要么已经是最终结果，要么可以继续计算。

保持定理（Preservation / Subject Reduction）：如果 Γ ⊢ e : T 且 e → e'，则 Γ ⊢ e' : T。即计算步骤保持类型不变。

两个定理合在一起保证了类型安全：一个良类型的程序在求值过程中永远不会"卡住"（stuck），即不会出现对值执行不适当操作的情况。这是类型安全语言的核心保证——通过类型检查的程序在运行时不会出现类型错误。

替换引理是证明保持定理的关键工具：如果 Γ, x:T1 ⊢ e : T2 且 Γ ⊢ v : T1，则 Γ ⊢ e[x := v] : T2。即类型正确的替换保持类型正确。

2.4 强规范化定理

强规范化定理（Strong Normalization）是 STLC 最深刻的元理论性质之一。它指出：每一个良类型的 STLC 项在有限步 beta 归约后都会达到范式（不可再归约的项）。换句话说，STLC 中不存在无限归约序列。

这个定理的证明使用了一种巧妙的技术——可归约性候选（reducibility candidates）或逻辑关系（logical relations）。基本思路是：为每个类型 T 定义一个"良行为"项的集合，然后证明所有良类型的项都属于对应类型的良行为集合。

强规范化定理的直接推论是：STLC 不是图灵完备的。在 STLC 中，所有程序都保证终止，因此无法表达无限循环或通用计算。这与无类型 lambda 演算形成鲜明对比——无类型 lambda 演算是图灵完备的，但无法保证程序终止。

这个限制意味着 STLC 无法直接编码 Y 组合子或递归函数。要支持通用计算，需要扩展类型系统——这正是后续章节要讨论的内容。

2.5 类型推导与合一

类型推导（Type Inference）是在不显式标注类型的情况下自动确定表达式类型的过程。对于 STLC 的一个扩展——Hindley-Milner 类型系统，存在高效的类型推导算法。

合一算法（Unification）是类型推导的核心。给定两个类型表达式 S 和 T，合一算法寻找一个替换 σ（将类型变量映射到类型），使得 σ(S) = σ(T)。如果这样的替换存在，则 S 和 T 是可合一的；最一般合一（Most General Unifier, MGU）是所有合一中最通用的那个。

例如，合一 a → b 和 (c → c) → d：首先将 a 与 c → c 合一，得到替换 [a := c → c]；然后将 b 与 d 合一，得到替换 [b := d]。最终 MGU 为 [a := c → c, b := d]。

Algorithm W 是 Hindley-Milner 类型系统的经典推导算法。它自底向上遍历表达式语法树，为每个子表达式引入类型变量，生成类型约束，然后通过合一求解约束。Algorithm W 能推导出主类型（Principal Type）——如果表达式有类型，Algorithm W 一定能找到最通用的那个。

三、深入分析

3.1 Curry-Howard 同构在 STLC 中的体现

STLC 与直觉主义命题逻辑之间存在精确的对应关系，这是 Curry-Howard 同构最简单的形式：

例如，类型 (A → B) → (B → C) → A → C 对应命题 "如果 A 蕴含 B，且 B 蕴含 C，则 A 蕴含 C"——这正是假言三段论。具有这个类型的程序 λf.λg.λx.g(f(x)) 就是这个命题的证明。

这个对应的深刻之处在于：类型检查等价于证明检查。编写一个类型正确的程序等价于构造一个逻辑证明。这为自动化定理证明提供了计算化的途径。

3.2 STLC 的表达能力与限制

STLC 虽然保证了终止性和类型安全，但其表达能力受到严格限制。具体来说：

可以表达的：所有有限深度的数据操作、所有可以用 if-then-else 表达的条件逻辑（通过 Church 编码布尔值）、所有有界循环（通过 Church 编码自然数，但只能做固定次数的迭代）。

不能表达的：一般递归函数（如阶乘、斐波那契数列的递归定义）、自解释器（STLC 不能解释自身）、Y 组合子或任何不动点组合子。

这些限制的根本原因在于强规范化定理：STLC 中所有程序都终止，因此无法表达可能不终止的计算。要突破这些限制，需要扩展类型系统：

• 添加递归类型或不动点组合子 → 获得通用计算能力，但失去强规范化
• 添加多态类型（System F）→ 获得参数多态，仍保持强规范化
• 添加依赖类型 → 获得更精细的类型表达，但类型检查变得更复杂

3.3 Church 风格 vs Curry 风格

类型化 lambda 演算有两种风格，对应不同的设计哲学：

Church 风格（显式类型化）：每个 lambda 抽象都带有类型注解 λx:T.e。类型是项的内在组成部分，同一个底层无类型项在不同类型注解下被视为不同的 Church 项。类型检查是局部的、确定性的。

Curry 风格（隐式类型化）：lambda 项本身不携带类型信息，类型是通过类型分配（typing assignment）从外部赋予的。同一个无类型项可能有多种类型分配，也可能没有类型分配。类型检查需要全局推导。

在实际编程语言中，Java 和 ML 更接近 Church 风格（要求显式类型标注），而 Haskell 和 TypeScript 更接近 Curry 风格（大量使用类型推断）。两种风格各有优劣：Church 风格更明确但冗余，Curry 风格更简洁但推导可能失败。

四、实践案例

4.1 案例一：实现类型检查器

让我们用伪代码实现一个简单的 STLC 类型检查器：

type Type = "Bool" | "Nat" | Arrow(Type, Type)

type Expr =
  | Var(string)
  | Abs(string, Type, Expr)
  | App(Expr, Expr)

type Context = Map<string, Type>

function typeCheck(ctx: Context, expr: Expr): Type {
  match expr {
    case Var(x):
      return ctx.lookup(x) or throw "unbound variable"
    case Abs(x, T, body):
      let bodyType = typeCheck(ctx + {x: T}, body)
      return Arrow(T, bodyType)
    case App(e1, e2):
      let t1 = typeCheck(ctx, e1)
      let t2 = typeCheck(ctx, e2)
      match t1 {
        case Arrow(paramType, returnType):
          if t2 == paramType then return returnType
          else throw "type mismatch in application"
        case _:
          throw "applying non-function type"
      }
  }
}

这个类型检查器直接实现了 STLC 的类型判断规则，是理解类型检查过程的最直接方式。

4.2 案例二：用 STLC 编码逻辑证明

利用 Curry-Howard 同构，我们可以在 STLC 中编码逻辑证明。例如，证明命题 (A ∧ B) → (B ∧ A)（合取交换律）：

-- 类型：(A × B) → (B × A)
-- 程序：λp. (snd p, fst p)
-- 证明：假设 A ∧ B，则 B（由 ∧-消去）且 A（由 ∧-消去），故 B ∧ A（由 ∧-引入）

再如，证明命题 A → ¬¬A（双重否定引入），其中 ¬A 编码为 A → ⊥：

-- 类型：A → (A → ⊥) → ⊥
-- 程序：λa.λf. f a
-- 证明：假设 A，假设 ¬A（即 A → ⊥），由 Modus Ponens 得 ⊥

这些例子展示了如何在编程中自然地构造逻辑证明，体现了 Curry-Howard 同构的实用价值。

五、常见误区

5.1 误区一：STLC 是图灵完备的

STLC 不是图灵完备的。强规范化定理保证了所有 STLC 程序都终止，因此无法表达通用计算。要获得图灵完备性，需要扩展 STLC（如添加不动点组合子、递归类型或一般递归）。

5.2 误区二：类型注解是多余的

在 Church 风格的 STLC 中，类型注解不是多余的。它们不仅是类型检查的输入，还决定了项的语义——同一个无类型项在不同类型注解下可能有完全不同的行为。此外，类型注解使得类型检查成为简单的局部操作，无需全局推导。

5.3 误区三：类型推断总能成功

即使在支持类型推断的语言中，类型推断也可能失败。对于 STLC 的扩展（如包含 let 多态的 HM 系统），虽然 Algorithm W 总能找到主类型，但对于更复杂的类型系统（如包含子类型、重载的系统），类型推断可能变得不可判定或需要额外的类型标注辅助。

5.4 误区四：强规范化意味着程序总是正确的

强规范化只保证程序终止，不保证程序计算了正确的结果。一个类型正确的 STLC 程序可能终止但返回错误的结果。类型安全保证的是"不会出现类型错误"，而不是"业务逻辑正确"。

5.5 误区五：STLC 只与学术有关

STLC 的核心概念直接体现在现代编程语言中。Java 的方法签名检查、TypeScript 的函数类型检查、Rust 的闭包类型推导，本质上都是 STLC 类型判断规则的应用。理解 STLC 有助于深入理解这些语言特性的设计动机和限制。

六、本章小结

本章系统讲解了简单类型 lambda 演算的核心概念和性质。STLC 通过在无类型 lambda 演算中引入类型注解和类型判断规则，获得了类型安全的保证。三条基本类型规则（变量、抽象、应用）构成了类型检查的基础。

强规范化定理是 STLC 最深刻的性质——所有良类型项都保证终止，这既是优点（程序可预测、可验证）也是限制（无法表达通用计算）。Curry-Howard 同构揭示了 STLC 与直觉主义命题逻辑之间的精确对应，使得类型检查等价于证明验证。

类型推导算法（如 Algorithm W）使得程序员不必手动标注所有类型，同时保持了静态类型的安全保障。Church 风格和 Curry 风格的区分为理解不同语言的类型化策略提供了框架。

STLC 的表达能力限制推动了我们探索更强大的类型系统。下一章将引入子类型关系，允许类型之间的灵活转换。后续章节将进一步探讨多态类型、递归类型和存在类型，逐步构建完整的类型理论知识体系。

七、思考题

请为以下 STLC 项推导类型：λf:(Nat→Nat).λx:Nat. f (f x)。它的类型是什么？

证明在 STLC 中不存在具有类型 (A → A → A) → (A → A) 的项（提示：考虑该类型的逻辑含义）。

请解释为什么 Y 组合子 λf.(λx.f(x x))(λx.f(x x)) 在 STLC 中不可类型化。具体说明在哪一步类型检查会失败。

利用 Curry-Howard 同构，写出以下命题的证明（即具有对应类型的 STLC 项）：

- (A → B) → (A → C) → A → (B × C)

- ((A → B) → A) → A（Peirce 定律的变体，提示：这个命题在直觉主义逻辑中不可证明）

设计一个 STLC 的扩展，使得它既能保证强规范化，又能表达所有在有限输入上终止的函数。这样的扩展存在吗？为什么？