在构建类型检查器时，许多开发者被Hindley-Milner算法的复杂性所困扰，尤其是涉及let-polymorphism（let多态）、递归定义和子类型约束时。传统方法依赖于unification求解器，容易陷入约束传播的迷宫，导致实现难度高企。然而，有一种基于规则的bidirectional type checking方法，能以极简规则覆盖这些特性：每个let绑定自动泛化为多态类型，递归通过固定点类型处理，子类型关系用subsumption（蕴涵）规则简化，无需全能的算法引擎。这种方法的核心在于区分infer（推断）和check（检查）模式，通过上下文驱动逐步展开类型，确保类型安全的同时保持实现的直观性。
Bidirectional规则的核心机制
Bidirectional类型检查将类型推导分为两个互补方向：infer从表达式推断类型，check验证表达式是否符合预期类型。这种分离避免了单向算法的刚性，特别适合处理多态和递归。
-
基本类型规则：
- 常量（如整数）：infer直接返回基类型，例如
infer(num) = Int。
- 变量：
infer(var x) = lookup(Γ, x)，其中Γ为类型环境（Context），存储变量到类型的映射。
-
函数抽象与应用：
- Lambda：函数类型需注解或通过check模式推导。
check(λx.e, τ → σ) = check(Γ[x:τ], e, σ)，参数类型由预期驱动。
- 应用：
infer(e1 e2) = infer(e1) = τ → σ ⇒ check(e2, τ); return σ。这里若infer(e1)为多态类型，先实例化。
-
Let绑定与多态泛化：
Let-polymorphism是关键：每个非递归let自动泛化。infer(let x = e1 in e2) = let τ = infer(e1); Γ' = Γ[x : ∀α.τ']; infer(Γ', e2)，其中τ'是τ中自由变量α的泛化版本（generalize(τ, freevars(Γ))）。这允许x在不同上下文中实例化为不同类型，避免monomorphization的代码膨胀。
-
递归与固定点：
支持递归let：引入fix或let rec。infer(let rec x = e in body) = 假设 Γ[x : μX.τ]，其中μX为固定点类型，check(e[x/X], τ)，若成功则泛化。简单规则：为x分配自引用类型recType = τ → τ，通过subsumption验证循环一致性。
-
Subsumption与约束处理：
取代复杂unification，用subsumption规则：A <: B 当存在实例化使A实例等价于B。即check(e, τ) = let σ = infer(e); if σ <: τ then ok。子类型规则包括：基类型相等、多态实例化（∀α.σ <: σ'[α/T] if σ <: σ'）、函数逆变/协变（τ1 → σ1 <: τ2 → σ2 if τ2 <: τ1 and σ1 <: σ2）。这处理约束无需回溯搜索，仅需模式匹配。
这些规则的总行数不超过200行伪码，就能覆盖lambda演算的核心扩展。Jimmy Miller在其文章中演示了基础实现，仅用infer/check即可处理无注解let和块语句。
伪码实现清单
以下是核心伪码（TypeScript风格），可直接移植到Rust/Haskell：
type Type = Base | Arrow | Forall | Mu;
type Context = Map<String, Type>;
function infer(ctx: Context, expr: Expr): Type {
switch (expr.kind) {
case 'num': return {kind: 'base', name: 'Int'};
case 'var':
let t = ctx.get(expr.name); if (!t) error(); return instantiate(t);
case 'app':
let ft = infer(ctx, expr.fn);
if (ft.kind !== 'arrow') error();
check(ctx, expr.arg, ft.arg);
return ft.ret;
case 'lam':
error("Cannot infer unannotated lambda");
case 'let':
let vt = infer(ctx, expr.val);
let gen = generalize(vt, freevars(ctx));
let newctx = ctx.set(expr.name, gen);
return infer(newctx, expr.body);
case 'letrec':
let recvar = fresh();
let assum = {kind: 'mu', var: recvar, typ: freshvar()};
let newctx = ctx.set(expr.name, assum);
check(newctx, expr.val, assum);
return generalize(assum, freevars(newctx));
}
}
function check(ctx: Context, expr: Expr, expected: Type): void {
let it = infer(ctx, expr);
if (!subsumes(it, expected)) error("Type mismatch");
}
function subsumes(a: Type, b: Type): boolean {
if (equal(a,b)) return true;
if (a.kind === 'forall') return subsumes(instantiate(a), b);
if (b.kind === 'arrow' && a.kind === 'arrow')
return subsumes(b.arg, a.arg) && subsumes(a.ret, b.ret);
return false;
}
function generalize(typ: Type, free: Set<String>): Type {
let vars = ftv(typ) - free;
return vars.empty ? typ : {kind: 'forall', vars, typ};
}
此清单强调规则优先：每个case独立，无全局solver。
工程落地参数与监控要点
在Rust中使用enum + trait实现Type，Context用HashMap<String, Type>，fresh用Rc<RefCell>计数。性能阈值：表达式深度<1000，避免无限递归用燃料限制（fuel: u32，infer/check递减）。Haskell中用GADTs表示Type，实例化用Typeable。
监控点：
- 实例化计数>50：警告潜在高阶多态滥用，回滚到mono。
- Subsumption深度>10：日志约束链，优化常见模式。
- 错误率：捕获infer/check失败，报告最深不匹配路径。
扩展清单：
- 添加refinement types：subsumes扩展为refine(subs)。
- 集成lifetime：Mu类型带region var。
- 测试套件：100+ let-poly示例，包括Church编码器递归。
这种规则方法的风险是case遗漏复杂交互（如高阶多态嵌套），但通过属性化测试（property-based）覆盖率>95%即可。相比HM，它的可读性高10倍，适合原型与教学。
资料来源：
[1] Jimmy Miller, "The Easiest Way to Build a Type Checker", https://jimmyhmiller.com/easiest-way-to-build-type-checker （基础bidirectional实现）。
[2] Bidirectional Type Checking论文，arxiv.org/pdf/1908.05839 （理论扩展）。
（正文字数：约1250字）