name: simply-typed-lambda-calculus description: ‘实现带有积、和和单位类型的简单类型化λ演算。使用场景：(1) 学习类型系统，(2) 构建解释器，(3) 形式化语言。’ version: 1.0.0 tags:

类型系统
λ演算
stlc
基础 difficulty: 初学者 languages:
python
ocaml
haskell dependencies:
lambda-calculus-interpreter

简单类型化λ演算

实现简单类型化λ演算（STLC）及其扩展。

何时使用

学习类型系统
构建解释器
形式化验证
语言原型设计

这个技能做什么

实现基础STLC - 函数、变量
添加积类型 - 对、投影
添加和类型 - 标记联合
证明健全性 - 进展 + 保持

如何使用

定义类型和项的语法
实现类型判断 Γ ⊢ e : τ
实现小步评估
为每个归约规则证明进展和保持

关键概念

概念	描述
函数类型	τ₁ → τ₂（箭头）
积类型	τ₁ × τ₂（对）
和类型	τ₁ + τ₂（标记联合）
单位	终端对象
健全性	进展 + 保持

扩展

扩展	描述
多态性	类型变量（系统F）
递归	不动点组合子
引用	可变状态
子类型	宽度/深度子类型

提示

从基础STLC开始
一次添加一个特性
增量证明健全性
使用德布鲁因索引进行绑定

经典参考文献

参考	为何重要
Barendregt, “The Lambda Calculus”	λ演算变体的权威参考
Pierce, “Types and Programming Languages”, Ch. 5-9	带有积、和、递归类型的STLC
Girard, Lafont, Taylor, “Proofs and Types”	系统F和类型理论基础
Mitchell, “Foundations for Programming Languages”	全面的类型系统覆盖

研究工具与工件

形式化STLC的证明辅助工具：

形式化	证明辅助工具	学习内容
TAPL in Coq	Coq	完整的健全性证明
Software Foundations	Coq	教学性开发
Homotopy Type Theory	Agda	高阶归纳类型
PFPL	Coq	Pierce的形式化

关键实现

OCaml的类型系统 - 工业级STLC带扩展
GHC Core - STLC带let浮动优化
STLC in Lean - 类型理论的元编程

研究前沿

1. 规范化

目标：证明评估总是终止
技术：逻辑关系、可约候选
论文：Girard, Lafont & Taylor “Proofs and Types”（第4-6章）；Tait方法
应用：证明辅助工具、终止检查

2. 项的表征

目标：在STLC中可定义的函数是什么？
关键结果：STLC项是强规范化的（没有递归/不动点时不图灵完备）
论文：“The Church-Rosser Property”（Curry & Feys）
技术：可约候选

3. 语义回读

目标：从正规形式重构项
技术：通过评估进行规范化（NbE）
论文：“Normalization by Evaluation”（Berger & Schwichtenberg）
应用：具体化、证明提取

实现陷阱

陷阱	症状	解决方案
缺少箭头类型情况	未检查的函数类型崩溃	在所有情况下处理TFun
错误的环境作用域	闭包捕获错误的值	深拷贝或逃逸分析
替换顺序	Alpha重命名冲突	使用德布鲁因索引
保持证明缺口	归约后类型变化	为每个规则证明引理

“类型保持非显然”的教训

每个评估规则都需要一个保持证明：

# 对于App：如果 ⊢ e1 : A→B 且 ⊢ e2 : A
#          且 e1 e2 → e'[e2/x]
#          则 ⊢ e'[e2/x] : B

# 需要替换引理：
# 如果 Γ, x:A ⊢ e : B 且 Γ ⊢ v : A
# 则 Γ ⊢ e[x↦v] : B

这就是为什么STLC健全性需要努力证明！

简单类型化λ演算Skill simply-typed-lambda-calculus