形式陈述

System F（多态 lambda 演算）在简单类型 lambda 演算上加入全称类型 $\forall\alpha.T$$\mathrm{\forall }\alpha .T$、类型抽象 $\Lambda\alpha.t$$\mathrm{\Lambda }\alpha .t$ 与类型应用 $t[A]$$t[A]$。核心规则为

$$ \frac{\Gamma,\alpha\ \mathrm{type}\vdash t:T}{\Gamma\vdash\Lambda\alpha.t:\forall\alpha.T}, \qquad \frac{\Gamma\vdash t:\forall\alpha.T}{\Gamma\vdash t[A]:T[A/\alpha]}. $$$$\frac{\mathrm{\Gamma },\alpha \mathrm{type}⊢t:T}{\mathrm{\Gamma }⊢\mathrm{\Lambda }\alpha .t:\mathrm{\forall }\alpha .T},\frac{\mathrm{\Gamma }⊢t:\mathrm{\forall }\alpha .T}{\mathrm{\Gamma }⊢t[A]:T[A/\alpha ]}.$$

类型级 $\beta$$\beta$ 归约满足 $(\Lambda\alpha.t)[A]\to t[A/\alpha]$$(\mathrm{\Lambda }\alpha .t)[A]\to t[A/\alpha ]$。纯 System F 具有保持性、进展性和强归一化；显式带类型标注的类型检查可判定，但一般类型重建或 typability 不可判定。

直觉

程序不仅抽象值参数，还抽象类型本身；调用者显式选择类型实例，而同一项在所有实例上保持统一结构。

例子与边界

多态恒等函数为 $\Lambda\alpha.\lambda x{:}\alpha.x$$\mathrm{\Lambda }\alpha .\lambda x:\alpha .x$，类型是 $\forall\alpha.\alpha\to\alpha$$\mathrm{\forall }\alpha .\alpha \to \alpha$。Church 编码可在 System F 中表示布尔值、自然数、积和部分递归数据。System F 的量词可嵌套在任意位置，比 HM 的秩一 let 多态更强，但这种表达力正使完整推断失去可判定性。加入一般递归后强归一化不再成立。

推论与应用

System F 是多态语言元理论、参数性和抽象定理的核心模型，也连接二阶直觉主义逻辑。现实语言通常采用可推断片段、显式泛型或更高秩扩展，在表达力与推断可行性之间折中。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chs. 23–24, System F syntax, typing, and metatheory。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Chs. 10–11, polymorphic type abstraction。