类型判断

上下文记录当前可用的静态假设，推导树给出类型结论的证据。判断中的冒号连接“项”与“类型”，横杠连接“前提判断”与“结论判断”；二者不是程序里的赋值。尤其是 $\mathrm{\Gamma },x:A$ 只告诉我们 $x$ 可按 $A$ 使用，并没有替 $x$ 提供运行时数值。

类型检查可以看成受约束的证明搜索：若目标项是应用 $fx$，最后一步必须解释一次调用，因此先寻找函数的箭头类型，再检查实参是否匹配其定义域。在这里列出的简单规则中，语法外形帮助选择最后规则；有转换或子类型规则时，最后一步未必如此唯一。

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

信息流类型系统理路信息流类型系统Information-flow type system · Security typing with a program-counter label用固定安全标签和pc规则排除显式与隐式低写入，并说明双运行可靠性和终止观察的边界。把上下文具体化为公开/秘密标签，并用pc记录控制选择。秘密条件中写公开常量也可能泄漏，因此赋值规则同时检查右端和pc；两支恰好写同一常量却仍被拒绝，则展示这种语法证明的保守性。

在 $\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}$。

同一上下文不能推出 $xf$ 的类型：应用规则要求左项 $x$ 有箭头类型，而唯一变量声明给它 $\mathbb{Z}$。这不是运行后发现整数不能调用，而是在构造推导时所需前提无法成立。反过来，$fx$ 的结果类型为布尔，并不告诉我们结果究竟是 true 还是 false；那需要函数的实现与动态语义。

“在某上下文中良类型”不保证可独立运行。$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对按值调用的简单类型 lambda 演算逐层解释规范形、替换、进展与保持，以及类型安全的准确结论。再把静态推导与动态执行连接起来。Hindley–Milner 推断从无注解项构造判断与主类型；证明助理中的类型检查器则验证证明项对应的判断。