双向类型检查

形式陈述 ​

双向类型系统把单一的声明式类型判断公理库类型判断Typing judgment在上下文中断言项具有某类型的形式判断。拆成两种算法化判断：

$$\mathrm{\Gamma }⊢e\Rightarrow A\text{与}\mathrm{\Gamma }⊢e\Leftarrow A.$$

$\Rightarrow$ 表示从上下文与项综合出类型，$\Leftarrow$ 表示在已经给定期望类型时检查项；箭头只是信息流方向，不是逻辑蕴含。对简单类型 λ 演算公理库简单类型 λ 演算Simply typed lambda calculus · STLC给 λ 演算加入基础类型与函数类型，从语法上排除一类无意义应用。，一组核心规则是

$$\frac{x:A\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x\Rightarrow A},\frac{\mathrm{\Gamma }⊢e_1\Rightarrow A\to B\mathrm{\Gamma }⊢e_2\Leftarrow A}{\mathrm{\Gamma }⊢e_1{e}_2\Rightarrow B},$$$$\frac{\mathrm{\Gamma },x:A⊢e\Leftarrow B}{\mathrm{\Gamma }⊢\lambda x.e\Leftarrow A\to B}.$$

变量和消去形式通常能从其主项得到输出类型，因而综合；λ 抽象等引入形式则利用期望类型检查其组成部分。两种方向由注解和可转换性规则连接：

$$\frac{\mathrm{\Gamma }⊢e\Leftarrow A}{\mathrm{\Gamma }⊢(e:A)\Rightarrow A},\frac{\mathrm{\Gamma }⊢e\Rightarrow AA\equiv B}{\mathrm{\Gamma }⊢e\Leftarrow B}.$$

后一规则把 synthesis 结果用于 checking；若系统含子类型，可把 $A\equiv B$ 换成相应 subsumption 条件。可转换性是否可判定、是否需要归一化，仍由底层类型理论决定。双向组织不会把一个不可判定的类型等价问题自动变成算法。

相对于声明式系统，soundness 陈述为：若双向判断成功，则擦除方向标记并保留或 elaboration 注解后，可得到声明式推导 $\mathrm{\Gamma }⊢|e|:A$。completeness 通常必须允许插入注解：若声明式 $\mathrm{\Gamma }⊢e:A$ 成立，则存在擦除后为 $e$ 的已注解项 $e^{\prime }$，使 $e^{\prime }$ 能在适当方向综合或检查 $A$。这两个方向分别是算法可靠性与完备性公理库算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。义务，不能含糊地合并成“两个系统等价”。若规则按项结构递归且类型可转换性可判定，还要另外证明检查过程终止，才能得到总的判定算法。

直觉 ​

有些语法自己携带足够信息。看到变量可查上下文，看到应用可先问函数是什么箭头类型；另一些语法需要目标才能理解，未注解的 λx.x 没说 $x$ 是整数、布尔还是任意 $A$。双向检查让信息从最自然的方向流动，只在信息即将断开的位置要求程序员或 elaborator 补一小块注解。

它不是一种新的类型理论，而是把声明式规则重新定向为可实现检查器的方法。同一依赖类型或多态系统可以有不同双向设计；哪些项综合、哪些项检查、何处插入注解，决定可用性和完备性表述。

例子与边界 ​

在期望类型 $A\to A$ 下，规则把 λx.x 的检查化为 $\mathrm{\Gamma },x:A⊢x\Leftarrow A$；变量先综合 $A$，再由可转换性规则完成检查。没有期望类型时，裸 λ 在上述系统中没有 synthesis 规则，因而不能独立推出它到底是哪一个恒等函数类型。

若上下文含 $f:A\to B$ 与 $x:A$，应用 f x 先由变量规则综合 $f$ 的箭头类型，再检查 $x\Leftarrow A$，最终综合 $B$。若需要让恒等 λ 进入综合位置，可写 (λx.x : A→A)；注解规则先检查内部项，再把 $A\to A$ 作为输出。

双向模式不解决 System F 的一般隐式高阶类型推断不可判定问题。它可以通过显式类型应用、局部注解和受限的 subsumption 设计一个可判定接口，但注解策略仍是语言设计的一部分。checking 也不总比 inference 简单：依赖类型中的 definitional equality、复杂子类型或隐式参数搜索仍可能昂贵甚至不可判定。

推论与应用 ​

双向检查把错误定位在信息流发生冲突的位置，适合交互式编辑器、证明助理和带丰富类型的语言。elaboration 还能在检查过程中插入类型应用、强制转换或核心注解；正确性要求生成的核心项在声明式系统中良类型，并与源项保持约定的运行语义。

与 Hindley–Milner 的全局约束推断相比，双向系统偏向局部传播已知类型，不承诺为所有无注解项寻找主类型。二者可以组合：局部表达式用统一变量解约束，构造边界仍按 synthesis/checking 方向组织；具体组合必须重新证明可靠性、完备性和终止性。

参考资料

• Jana Dunfield and Neel Krishnaswami, “Bidirectional Typing,” ACM Computing Surveys 54(5), 2021。
• Benjamin C. Pierce and David N. Turner, “Local Type Inference,” ACM TOPLAS 22(1), 2000。
• Frank Pfenning, “Bidirectional Typing,” lecture notes, Carnegie Mellon University，algorithmic typing judgments and mode discipline。