形式陈述

类型判断通常写作

$$ \Gamma\vdash t:T, $$$$\mathrm{\Gamma }⊢t:T,$$

表示在类型上下文 $\Gamma$$\mathrm{\Gamma }$ 中，项 $t$$t$ 具有类型 $T$$T$。它由语法导出规则归纳定义；判断成立当且仅当存在以该判断为结论的有限推导树。上下文记录自由变量的类型假设。

直觉

类型判断不是运行时测试结果，而是形式系统中的可导出断言。规则同时描述语言构造如何使用以及哪些程序在执行前被拒绝。

例子与边界

在简单类型 $\lambda$$\lambda$ 演算中，由 $\Gamma,x:S\vdash t:T$$\mathrm{\Gamma },x:S⊢t:T$ 可推出 $\Gamma\vdash\lambda x.t:S\to T$$\mathrm{\Gamma }⊢\lambda x.t:S\to T$；由 $\Gamma\vdash f:S\to T$$\mathrm{\Gamma }⊢f:S\to T$ 与 $\Gamma\vdash s:S$$\mathrm{\Gamma }⊢s:S$ 推出 $\Gamma\vdash f\,s:T$$\mathrm{\Gamma }⊢fs:T$。不同类型系统可对同一语法给出不同判断。

推论与应用

进展与保持定理量化可导出的类型判断，类型推断则尝试构造此类推导。判断形式也推广到效应、子类型和程序逻辑。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002, Statics chapters。
• Andrew K. Wright and Matthias Felleisen, “A Syntactic Approach to Type Soundness,” Information and Computation 115(1), 1994, Chapters 8–11。