形式化方法导引主线 13 篇结束后，常被问的延伸问题是："Curry-Howard 同构是不是只有’逻辑 ↔ 类型’这两端？"答案是不完全：1980 年前后 Lambek 把这条同构补成了一个三角——加入范畴论作为第三个等价表述。

逻辑、类型论、范畴论说的是同一件事，只是观察镜头不同。这条三角对应被叫 Curry-Howard-Lambek 同构，是任何想往程序语言语义、依值类型基础、同伦类型论方向走的人必须越过的一座山。

本文是系列附录，不属于主线 13 篇，目的是给硕士生指一条范畴论入门的最短路径。不展开范畴论基础，重点把"三角"的形态点清楚。

三角的形态

1
2
3
4
5
6
7
8
9
10
11
12
      逻辑 (直觉主义命题逻辑 IPC)
               /\
              /  \
             /    \
            /      \
           /        \
          /          \
         /            \
        /              \
       /                \
    类型论 ——————— 范畴论
(STLC, 依值类型)   (笛卡尔闭范畴 CCC)

每两端之间都有一条"翻译"，三条翻译两两可逆，构成等价：

翻译 方向
命题 ↔ 类型 Curry-Howard（第 02 篇主题）
类型 ↔ 范畴对象 Lambek 1980
命题 ↔ 范畴对象 通过另两条复合

任何一段良类型程序在三种镜头下都有对应物：

  • 逻辑视角：一棵自然演绎树。
  • 类型视角：一个 STLC 项。
  • 范畴视角：笛卡尔闭范畴中的一支态射。

范畴论的最小词汇

不熟悉范畴论的读者可以先记住六个词：

词 含义 类型论对应
范畴 (category) 对象与态射的集合，态射可组合，有恒等 类型 + 函数
对象 (object) 范畴中的"点" 类型
态射 (morphism) 从 A 到 B 的"箭头" 函数 f : A → B
恒等态射 (identity) id_A : A → A fun x : A => x
复合 (composition) g ∘ f : A → C fun x => g (f x)
积 (product) A × B 加投影 元组类型 + fst / snd

把"类型"当成对象、"函数"当成态射，CS 学生已经在用范畴论了——只是没用过这个名字。

笛卡尔闭范畴 = STLC 的语义

笛卡尔闭范畴（Cartesian Closed Category，CCC）是有以下结构的范畴：

  1. 有终对象 1。
  2. 任意两个对象有积 A × B，配套投影 π1、π2。
  3. 任意两个对象有指数对象 B^A（也写作 A ⇒ B），配套 eval : (B^A) × A → B，满足以下泛性质：对任意 f : C × A → B，存在唯一 λf : C → B^A 使 eval ∘ (λf × id) = f。

把这三条对照 STLC 的类型：

CCC 概念 STLC 类型 / 项
终对象 1 Unit，()
积 A × B 积类型，(a, b)，fst / snd
指数 B^A 函数类型 A → B，fun a => ...，函数应用
恒等态射 id_A fun x : A => x
复合 g ∘ f fun x => g (f x)
eval 函数应用
柯里化 λf fun c => fun a => f (c, a)

Lambek 1980 的定理：STLC 与 CCC 之间存在对应——STLC 的良类型项空间作为一个语法范畴，正是某种 CCC 的内部语言。反过来，任何 CCC 的态射都可以用 STLC 项表示。

这条定理把"程序"重新读成"范畴中的箭头"。一段 STLC 程序的执行（β-规约）对应范畴中的态射相等（在合适的等价关系下）。

三角的工程价值

读到这里，CS 学生可能会问：“多一条等价表述对工程有什么用？”

三条价值：

一、范畴论给类型系统提供数学语义

任何新类型系统（多态、依值、线性、量子）在设计阶段都希望有一个数学模型，证明它"合理"。范畴论提供这样的模型。例如：

  • STLC 的语义是 CCC。
  • System F 的语义是 PL-category（一种 fibered category）。
  • 依值类型的语义是 locally cartesian closed category（LCCC）。
  • 线性类型的语义是 symmetric monoidal closed category。
  • 同伦类型论的语义是 ∞-topos 或 cubical model。

每条对应让"我设计的类型系统是不是自相矛盾"被简化为"是否存在一个非空模型"。

二、Monad / Functor / Applicative 等模式是范畴论原语

Haskell、Scala、Kotlin、Rust 里耳熟能详的 map / flatMap / Functor / Monad / Applicative / Traversable 这些抽象，是范畴论的直接翻译：

编程概念 范畴论对应
Functor 同名
Monad 同名（Kleisli 三元组）
Applicative lax monoidal functor
Comonad 对偶
Lens optic（cartesian / co-cartesian 配对）
Either / Sum 余积 (coproduct)
Pair / Tuple 积 (product)

工业上用 Cats / Scalaz / fp-ts 这些库的工程师，正在使用 70 年代抽象代数研究的产物。理解范畴论让这些模式不再是"散落的诀窍"，而是统一框架下的实例。

三、同伦类型论与立方类型论的入口

主线第 09 篇提到 Lean 4 接受 propext、Quot.sound、Classical.choice 等公理。这些公理在 HoTT（同伦类型论）里被定理替换，前提是接受 Univalence 公理。HoTT 的语义模型是 ∞-topos，理解这层语义需要范畴论基础。

立方类型论是 HoTT 的可计算变体（Cubical Agda 实现）。它的语义模型是 cubical sets，本质上是范畴论中的 presheaf category。

任何想往"形式化数学下一代基础"方向走的人，范畴论是必经之路。

一条最短入门路径

范畴论资料汗牛充栋，但适合 CS 学生的入门书不多。推荐顺序：

  1. Bartosz Milewski. Category Theory for Programmers. https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
    • 完全免费，从 Haskell 视角写起，CS 学生最易上手。
  2. Tom Leinster. Basic Category Theory. Cambridge, 2014.
    • 数学家写法，简洁，约 200 页。
  3. Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971.
    • 经典，但跳跃大，推荐当辞典而不是教材。
  4. Steve Awodey. Category Theory. Oxford, 2010.
    • 适合数学背景较强的读者，包含逻辑与范畴论的连接。
  5. Emily Riehl. Category Theory in Context. Dover, 2017.
    • 免费 PDF 在作者主页，覆盖现代视角。

每本读完一章就配套写一段 Lean / Haskell / Scala 代码实现该章概念，能极大降低"范畴论看上去抽象"的学习障碍。

在 Lean 4 里见到范畴论

Mathlib4 的 Mathlib.CategoryTheory.* 命名空间包含完整范畴论形式化：

1
2
3
4
5
6
7
8
9
import Mathlib.CategoryTheory.Category.Basic

open CategoryTheory

variable {C : Type*} [Category C]

example (X Y Z : C) (f : X ⟶ Y) (g : Y ⟶ Z) : X ⟶ Z := f ≫ g

example (X : C) : X ⟶ X := 𝟙 X

⟶ 是范畴中的"箭头"语法，≫ 是态射复合，𝟙 是恒等态射。Lean 4 把范畴论的所有公理（结合律、恒等律）当作类型类约束。

要在 Mathlib 范畴论生态里写一段简单的 functor：

1
2
3
4
5
6
7
8
import Mathlib.CategoryTheory.Functor.Basic

structure MyFunctor (C D : Type*) [Category C] [Category D] where
  obj : C → D
  map : ∀ {X Y : C}, (X ⟶ Y) → (obj X ⟶ obj Y)
  map_id : ∀ X, map (𝟙 X) = 𝟙 (obj X)
  map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    map (f ≫ g) = map f ≫ map g

这段定义直接把数学定义复刻到 Lean 4。同样的定义在 Mathlib 里写作 CategoryTheory.Functor，加了大量自动化设施。

Curry-Howard-Lambek 三角的两个直接练习

  1. 在自己的 Lean 4 工程里把"恒等函数复合一个普通函数等于该函数"用 Mathlib 的范畴论符号写一遍：

    1
    2
    example {C : Type*} [Category C] {X Y : C} (f : X ⟶ Y) :
        𝟙 X ≫ f = f := by simp

    思考这条等式在三种镜头下分别是什么命题。

  2. 用 Bartosz Milewski 的方式：把 Maybe / Option 实现的 functor 完整写出来。包括 fmap、map_id、map_comp。再思考为什么 Java 的 Optional<T> 严格说不是 functor（提示：方法链调用与组合律对应吗）。

三角告诉我们的一句话

回到 Lambek 三角，三个镜头底层是同一个对象：

镜头 看到什么
逻辑 一棵自然演绎树
类型 一段良类型 STLC 项
范畴 一支 CCC 中的态射

三者之间的等价不是"巧合"。它告诉我们：

直觉主义逻辑的"证明"、类型论的"程序"、范畴论的"态射"在结构上是同一类东西。

这条洞见 50 年来塑造了程序语言研究、形式化方法、范畴论本身的发展。它也是为什么 Lean 4 / Coq / Agda 能在同一套语法里同时处理"程序"和"证明"——这两件事在数学上本来就是同一件。

给系列读者的最后一句

主线 13 篇回答了"为什么编译通过就是定理得证"。本附录把这条等式接到第三条腿：范畴论。如果读者还想往下走：

  • 程序语义 → Bartosz Milewski、Pierce 的 TaPL
  • 高阶逻辑形式化 → Isabelle/HOL 与 Mathlib4
  • 同伦类型论 → HoTT Book、Cubical Agda、Coq HoTT
  • 范畴论本身 → Leinster、Awodey、Riehl

整个系列到此真正结束。形式化方法是一座大山，本系列是山脚到山腰的一条路。山腰之上，需要每位读者按自己的方向继续前进。

参考资料