形式陈述

类型由 $T::=\iota\mid T\to T$$T::=\iota \mid T\to T$ 生成。类型判断 $\Gamma\vdash t:T$$\mathrm{\Gamma }⊢t:T$ 按规则推导；例如若 $\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$。

直觉

类型记录函数期望和返回的对象类别，使“把布尔值当函数调用”这类错误在执行前被拒绝。

例子与边界

恒等函数 $\lambda x.x$$\lambda x.x$ 可具有 $T\to T$$T\to T$ 类型。无递归扩展的 STLC 中，每个良类型项都强正规化；因此它不能直接表达所有一般递归程序。

推论与应用

STLC 是现代静态类型语言、逻辑框架和更强类型系统的教学与理论核心。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, Chapters 8–9.
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Chapter 10.