双向类型检查

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

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

双向类型检查把规则分成“由项合成类型”和“用已知类型检查项”，通常依赖局部注解控制高阶特性；Hindley–Milner 类型推断理路Hindley–Milner 类型推断Hindley–Milner type inference · HM type system为带 let 的秩一参数多态 λ 演算提供主类型性质与可判定类型推断的系统。通过全局约束生成、合一与泛化为 ML 核心语言推导主类型。两者的完备范围与注解责任不同。

在期望类型 $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 方向组织；具体组合必须重新证明可靠性、完备性和终止性。

Π/Nat/Vec小核心理路依赖类型 elaborationDependent type elaboration · Elaboration of dependent types将表面程序展开为分层Π/Nat/Vec核心，以显式消去子构造向量连接，并由独立核重新检查motive、分支与conversion。选择全部λ参数显式注解，因此内核可综合每种构造，再用conversion检查期望类型；表面层仍可用双向信息流补全这些注解。实例明确分开表面推断、生成的消去项和独立重检的责任。