name: 类型检查器生成器 description: ‘从语言规范生成类型检查器。使用场景：(1) 设计新编程语言，(2) 为解释器添加类型检查，(3) 实现核心语言证明，(4) 构建语言原型。’ version: 1.0.0 tags:

类型系统
类型检查
编译器
静态分析 difficulty: 中级 languages:
python
ocaml dependencies:
lambda-calculus-interpreter

类型检查器生成器

从形式化类型系统规范生成健全且完整的类型检查器。

何时使用

设计新编程语言
从研究论文实现类型系统
构建带有静态类型检查的解释器
证明类型健全性属性
创建最小可行语言 (MVLs)

此技能的作用

解析类型系统规范 - 读取形式化规则（类型判断）
生成类型检查器代码 - 产生可执行的类型检查器
证明健全性 - 输出进展 + 保持证明草图
处理边缘情况 - 为类型错误生成错误消息

如何使用

为您的语言指定语法和声明式类型规则
编码算法检查规则（需要时添加推断）
为多态性添加替换/统一支持
通过正面/负面测试和元理论检查验证

关键概念

类型系统组件

组件	描述
语法	类型 (τ) 和项 (e)
类型规则	判断 (Γ ⊢ e : τ)
子类型	类型排序 (τ₁ <: τ₂)
种类化	类型级良好形式
类型错误	带有位置的错误消息

健全性定理

一个类型系统是健全的如果：

进展：一个良好类型的项要么是一个值，要么可以迈出一步
保持：如果 ⊢ e : τ 且 e → e’，那么 ⊢ e’ : τ

实现模式

结构

class TypeChecker:
    def __init__(self, type_system: TypeSystem):
        self.type_system = type_system
        self.context = {}
        self.errors = []
    
    def check(self, term: Term) -> Optional[Type]:
        """主入口点：检查项是否良好类型"""
        pass
    
    def check_app(self, func: Term, arg: Term) -> Optional[Type]:
        """使用 T-App 规则检查应用"""
        pass
    
    def unify(self, t1: Type, t2: Type) -> bool:
        """统一两个类型（用于推断）"""
        pass

错误报告

def type_error(self, term: Term, expected: Type, actual: Type):
    self.errors.append(TypeError(
        location=term.location,
        message=f"预期 {expected}，得到 {actual}"
    ))

常见模式

双向类型检查

分离为：

检查：给定 τ，验证 e : τ（更容易）
推断：给定 e，推断 τ（更难）

def synth(self, e: Term) -> Optional[Type]:
    """合成/推断模式"""
    match e:
        case Var(x): return self.lookup(x)
        case App(e1, e2):
            t1 = self.synth(e1)
            t2 = self.check(e2, t1.param_type)  # 检查与预期匹配
            return t1.return_type

def check(self, e: Term, tau: Type) -> bool:
    """检查模式"""
    match e:
        case Lam(x, body):
            self.check(body, tau.body)  # 泛化
        case _:
            tau' = self.synth(e)
            return tau' <= tau  # 子类型检查

基于约束的类型检查

在遍历期间收集约束，之后解决：

def infer(self, e: Term) -> (Type, Constraints):
    constraints = []
    match e:
        case App(e1, e2):
            t1, c1 = self.infer(e1)
            t2, c2 = self.infer(e2)
            fresh = fresh_type_var()
            constraints.append((t1, Fun(t2, fresh)))
            return (fresh, c1 ++ c2 ++ constraints)

提示

从简单类型 lambda 演算 (STLC) 开始
添加积、和，然后多态性
在实现过程中证明健全性
使用双向类型检查以获得更好的错误消息
跟踪源位置以生成有意义的错误

常见问题

问题	解决方案
无限类型	使用出现检查
递归类型	添加 μ（不动点）或等递归
子类型复杂性	从名义子类型开始，稍后添加结构子类型
错误消息	跟踪项位置，使用统一

权衡与限制

设计权衡

方法	优点	缺点
双向	更好的错误消息，更简单的实现	比基于约束的方法表达性差
基于约束	更灵活，主类型	复杂的约束解决
声明式	易于阅读规范	难以高效实现

何时不使用此方法

对于非常大的代码库：考虑将类型检查器作为单独服务
对于渐进类型：使用渐进类型推断代替（不同算法）
对于依赖类型：需要定理证明；参见 dependent-type-implementer 技能
对于行多态性：参见专门的 row-polymorphism 技能

限制

健全性与完备性：类型检查器通常是健全的（拒绝一些有效程序），但对于丰富类型系统，完备检查是不可判定的
错误本地化：精确的错误位置需要在整个过程中跟踪源
增量检查：未内置；需要单独的基础设施

评估标准

高质量类型检查器实现应具有：

标准	检查点
健全性	从不接受类型不良的程序
完备性	接受所有良好类型程序（当可判定时）
错误消息	清晰、本地化、可操作
类型推断	可能时主类型
效率	对于典型程序线性时间
可扩展性	易于添加新类型构造器
测试	基于属性的推断测试

质量指标

✅ 良好：通过所有良好类型程序，拒绝类型不良程序，产生清晰错误 ⚠️ 警告：覆盖不全，神秘错误消息，无推断 ❌ 不良：健全性错误，对有效输入崩溃

经典参考文献

参考文献	重要性
Pierce, “Types and Programming Languages”	类型系统权威教科书；第 8-15 章涵盖类型检查基础
Wright & Felleisen, “A Syntactic Approach to Type Soundness”	进展 + 保持证明技术
Cardelli, “Type Systems”	类型系统设计空间的全面调查
Girard, “Linear Logic”	线性类型和资源管理的基础
Hindley, “Basic Simple Type Theory”	多态性的经典参考

研究工具与工件

对于实现类型检查器，参考这些研究级实现：

工具	语言	学习内容
OCaml 编译器 (ocaml/ocaml)	OCaml	工业强度类型推断、模块系统、GADTs
GHC Haskell	Haskell	类型推断、类型类、角色系统
TypeScript 编译器 (microsoft/TypeScript)	TypeScript	渐进类型、联合类型、推断
Rust 编译器 (rust-lang/rust)	Rust	借用检查、特质系统、生命周期
Pyright	Python	Python 类型存根、渐进类型
Dafny 验证器	Boogie	验证集成类型检查

Coq 形式化（用于验证）

“Types and Programming Languages” in Coq - TAPL 的完整形式化
Coq’s kernel - 认证类型检查器实现
Iris (MPI-Freiburg) - 高阶分离逻辑

研究前沿

当前类型检查的活跃研究方向：

1. 渐进类型与可靠性

关键论文：“Gradual Typing for Functional Languages” (Siek & Taha, 2006), “Reticulated Python” (Vitousek et al.)
挑战：无缝融合静态和动态类型
工具：Pyre (Facebook), mypy, TypeScript

2. 双向类型检查

关键论文：“Reconstructing Type Inference” (Dunfield & Krishnaswami, 2023)
挑战：平衡推断能力与错误消息
工具：Agda, Idris, Deduce

3. 效应系统与能力

关键论文：“Koka: Programming with Row Polymorphic Effect Types” (Leijen, 2017)
挑战：无单子跟踪副作用
工具：Koka, Frank, Eff

4. 限定类型与类型类

关键论文：“How to Make Ad-hoc Polymorphism Less Ad-hoc” (Wadler & Blott, 1989)
挑战：不违反参数性的重载
工具：GHC Haskell, PureScript

实现陷阱

生产类型检查器实现中的常见错误：

陷阱	真实示例	预防
值限制	ML 的原始 let 多态性允许不健全	实现值限制 (Wright, 1995)
统一变量作用域	GHC 的未解决类型变量泄漏	维护基于级别的作用域跟踪
出现检查遗漏	无限类型如 `x = List(x)`	始终实现出现检查
子类型传递性	复杂层次结构导致健全性错误	系统地测试边缘情况
种类推断	类型级计算错误	实现单独的种类检查
推断中的无限循环	递归类型定义	添加深度限制并生成良好错误消息

“值限制” 故事

原始 Hindley-Milner let 多态性是不健全的：

(* 在原始 ML 中不健全 *)
let pair = (ref [], ref []) in
let (a, b) = pair in
  a := [1];  (* 添加整数到列表 *)
  b := [true]  (* 现在 a 包含布尔值！ *)

解决方案：仅对值绑定进行泛化（不对函数参数）。这就是为什么在 OCaml 中 let 和 let rec 语义不同。

主类型并非总是主类型

即使使用 Hindley-Milner，某些程序也没有主类型。知道何时报告歧义与尝试更多：

-- 哪个类型是主类型？
f x = [x, x + 1]  -- [Int] 或 [Num a]？

类型检查器生成器Skill type-checker-generator