类型判断

上下文记录当前可用的静态假设，推导树给出类型结论的证据。类型检查可以看成受约束的证明搜索：从目标判断反向选择规则，再为每个前提构造子推导。

这项证明只使用静态可见信息，不运行所有可能输入。类型系统因而通常是保守近似：可推导项获得保证，一些实际运行安全却无法在当前规则中证明的项仍会被拒绝。

在 $\mathrm{\Gamma }=x:\mathbb{Z},f:\mathbb{Z}\to \mathbb{B}$ 中，可直接构造

对闭项 $\lambda x:\mathbb{Z}.x$，函数体在临时上下文 $x:\mathbb{Z}$ 下定型，抽象规则解除该假设后得到 $\varnothing ⊢\lambda x:\mathbb{Z}.x:\mathbb{Z}\to \mathbb{Z}$。

“在某上下文中良类型”不保证可独立运行。$x+1$ 在 $x:\mathbb{Z}$ 下可定型，却仍含自由变量；进展定理若针对闭程序，就不能直接应用它。类型判断也不声称项会终止，更不描述运行时值。

声明式规则未必直接给出算法。带完整注解、语法导向的规则常可机械反推；子类型、隐式多态或依赖类型相等会引入搜索与约束求解。双向类型检查公理库双向类型检查Bidirectional type checking · Bidirectional typing把类型综合与给定类型下的检查分开，并用局部注解连接两种方向的算法化类型判断。通过区分综合与检查，重新组织相同或相近的声明式内容。

类型判断直接作用于语法项与上下文，不依赖某种编译器AST 表示公理库抽象语法树Abstract syntax tree · AST把抽象语法构造表示为有根有序树的常见编译器数据结构。。简单类型 λ 演算公理库简单类型 λ 演算Simply typed lambda calculus · STLC以基础类型和箭头类型约束 λ 项，获得类型安全与强正规化的最小函数演算。、System F 和依赖类型理论通过不同规则定义各自的合法项。

元理论通常对类型推导归纳。逆置引理从结论判断恢复最后规则可能提供的前提，替换引理处理 β-步骤，进展与保持定理公理库进展与保持定理Progress and preservation · Type safety在固定动态语义下，良类型闭项可继续或已是结果，且每一步都保持其类型。再把静态推导与动态执行连接起来。Hindley–Milner 推断从无注解项构造判断与主类型；证明助理中的类型检查器则验证证明项对应的判断。