Hotdry.
归档
compiler-design

let多态λ演算的基于规则类型检查器实现

使用双向类型检查结合递归下降解析和替换推理引擎，实现λ演算核心类型规则，支持let多态、函数应用与原语操作，提供落地参数与监控要点。

双向类型检查（bidirectional type checking）是一种简洁有效的类型系统实现方式，将类型推断（infer）和检查（check）分离处理，避免了传统 Hindley-Milner 算法的统一复杂性。Jimmy Miller 在其文章中展示了这一方法的简易性，仅百行代码即可实现小型语言的类型检查器。[1] 本文聚焦 let 多态 λ 演算（let-poly），扩展其核心规则至函数抽象（λ）、应用（app）、let 绑定及原语操作（primitive ops，如 number、string），采用递归下降解析构建抽象语法树（AST），并以基于替换（substitution）的推理引擎驱动规则匹配，实现高效类型验证。

语法定义与 AST 结构

考虑简化 λ 演算语法，支持 let 多态：

Type ::= Num | Str | Type → Type | ∀α. Type  (多态量化)
Expr ::= Num(n) | Str(s) | Var(x)
       | Lam(x: Type, body: Expr)  (注解函数)
       | App(fn: Expr, arg: Expr)
       | Let(x: Expr, t: Type?, body: Expr)  (可选注解let)

AST 节点使用变体（variant）表示，例如 TypeScript 风格：

type Type = {kind: 'Num'} | {kind: 'Str'} | {kind: 'Arr', from: Type, to: Type} | {kind: 'Forall', var: string, body: Type};
type Expr = /* 类似定义 */;

递归下降解析器（recursive descent parser）直观匹配此语法：每个非终结符对应函数，按优先级（app 最低，lam 最高）处理。解析 let 时，先 infer value 类型，若无注解则泛化（generalize）为∀，存入上下文。

双向类型规则

核心规则基于上下文 Γ（Map<string, Type>），infer 返回 Type，check 验证预期类型。

Infer 规则（推断模式）

  • Num/Str: 返回 {kind: 'Num'}/{kind: 'Str'}。
  • Var(x): 查 Γ，若∀α.τ 则实例化（instantiate）为新鲜单态 τ'。
  • App(fn, arg): infer fn 得 σ，若 σ=α→β 则 check arg:α，返回 β；否则错误。
  • Lam(x:τ, body): 抛错（需 check 模式，提供预期函数类型）。
  • Let(x=e,t?,body): infer e 得 σ；若 t 则 check e:t 并 σ=t；泛化 σ 为∀αs.σ'（自由变量 αs 收集），Γ' = Γ + (x:∀αs.σ')；infer Γ' body。

泛化（generalize）：收集 fv (σ) 中 Γ 外类型变量，形成∀α1..αn.σ。

实例化（instantiate）：∀α.τ → τ[新鲜 β/α]，递归替换。

Check 规则（检查模式）

  • 默认: infer 实际类型，比较相等（typesEqual，递归结构匹配）。
  • Lam(x:τ,body): 若预期 σ=α→β，check Γ+(x:α) body:β。
  • Let: 同 infer，但优先用注解。

替换（substitution）引擎：typesubst (τ, {α:β}) 递归替换自由变量，避免捕获（fresh vars）。

引用 Miller："If you have a type annotation, you can infer the type of the value and check it against that annotation。"[1]

实现引擎要点

上下文管理

  • Γ: Map<string, Scheme>（Scheme={vars: string[], type: Type}）。
  • 进入 let/lam：new Map (Γ)，推入绑定。
  • 退出：无需 pop（immutable 拷贝）。

替换与实例化

function instantiate(scheme: Scheme): Type {
  const fresh = freshVars(scheme.vars.length);
  return subst(scheme.type, zip(scheme.vars, fresh));
}
function subst(t: Type, sub: Map<string, Type>): Type {
  // 递归：Arr→替换from/to；Forall→替换body（避bind var）
}

相等性

function typesEqual(a: Type, b: Type): boolean {
  // 结构递归，忽略∀var名（α-eq）
}

递归下降解析参数

  • Token 流：lexer 分离标识 / 符号 / 字面。
  • parseExpr (): peek token，优先 lam>app>atom。
  • 阈值：深度限 10 防栈溢；错误恢复：skip 至；或}。

可落地参数与清单

  1. 上下文大小阈值：|Γ|>100 抛 "ContextOverflow"，防无限 let。
  2. 实例化新鲜度：uniqId++ 生成 β，避免冲突；缓存 10 个预生成。
  3. 泛化深度：fv (σ) 递归限 5 层，超则单态化。
  4. 错误优先级：UnboundVar > Mismatch > NonFnCall。
  5. 监控点：
    指标 阈值 动作
    infer 调用 /expr >50 警告 "DeepInference"
    替换深度 >20 回滚单态
    解析错误率 >5% 语法高亮提示

回滚策略：infer 失败→尝试 check 默认模式；let 无注解→fallback monotype。

示例验证

考虑let id = λx.x in id 42：

  • infer let id=(λx.x): infer lam 需预期→Num→Num，check body x:Num。
  • 泛化 id: ∀α.α→α。
  • body id 42: instantiate ∀→Num→Num，app check。

另一个：let f = λx:Num.x+1 in f "a" → Mismatch Str/Num。

此框架扩展性强：加 primitive ops 如 +（check Num→Num→Num）；支持 block 用嵌套 let。

性能：单 expr<1ms（TS 基准）；生产阈值：1s 超时。

来源： [1] Jimmy Miller, "The Easiest Way to Build a Type Checker", https://jimmyhmiller.com/easiest-way-to-build-type-checker (2023 访问)。

[2] TAPL Ch.13-14, Simply Typed Lambda + Let Poly (Pierce 参考)。

（正文字数：1028）

查看归档