System F

简单类型 λ 演算要求每个函数固定在某个具体参数类型上，System F 允许函数再对类型本身抽象。$\mathrm{\Lambda }\alpha$ 表示“接下来这段程序对任意类型 $\alpha$ 都成立”，类型应用则选择一个实例。impredicativity 的力量在于多态值可以用含全称量化的类型实例化，这带来丰富编码；当类型抽象与实例化位置不再显式给出时，推断问题也随之越过可判定边界。类型参数在运行时通常可擦除，因为纯 System F 项不能检查它到底是哪种类型。

多态恒等函数

具有类型 $\mathrm{\forall }\alpha .\alpha \to \alpha$。若增加布尔基类型及其常量，归约分两步：$\mathsf{id}[\mathbb{B}]\mathsf{true}\to (\lambda x:\mathbb{B}.x)\mathsf{true}\to \mathsf{true}$。第一步替换类型，第二步替换项；纯语法中的布尔也可用 Church 编码给出，其类型是 $\mathrm{\forall }\alpha .\alpha \to \alpha \to \alpha$，自然数可赋类型 $\mathrm{\forall }\alpha .(\alpha \to \alpha )\to \alpha \to \alpha$。

令 $I=\mathrm{\forall }\alpha .\alpha \to \alpha$，则 $\mathsf{id}[I]:I\to I$，所以 $\mathsf{id}[I]\mathsf{id}:I$ 良类型并归约到 $\mathsf{id}$。这里把一个多态类型传给类型参数，具体展示了 impredicative 实例化；它与无类型项 $xx$ 不同，应用前有明确的类型实例化步骤。

边界是把 System F 与 Hindley–Milner 混同。前者允许多态参数在任意位置并要求显式类型抽象，表达力更强；后者主要在 let 绑定处作秩一泛化，因而拥有主类型与可判定推断。

纯 System F 的强正规化还依赖没有一般递归；加入固定点算子后仍可维持进展与保持，却会立即失去“所有良类型项都终止”的结论。

System F 是参数多态理路参数多态Parametric polymorphism程序对类型参数统一工作而不依赖其具体表示的多态。的标准核心演算，许多泛型语言的中间表示都可翻译到它或其扩展。关系参数性理路关系参数性Relational parametricity · Reynolds parametricity · Abstraction theorem多态项必须统一保持类型之间任意关系的抽象定理及其行为约束。是关于良类型 System F 项保持任意关系的抽象定理，不反向成为演算语法的前置。存在类型理路存在类型Existential type · Existentially quantified type隐藏一个见证类型及其实现值，只允许客户端通过公开接口使用该表示的量化类型。可在 impredicative System F 中通过全称量化编码，并为抽象表示提供隐藏接口；原生 pack/unpack 的规则仍应与该编码区分。

其强正规化连接类型化正规化理路简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个良类型简单 λ 项都强正规化：任意完整 β-归约路径都在有限步后结束。与二阶直觉主义逻辑；在Curry–Howard 对应理路Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。下，System F 对应二阶命题逻辑。

现代编译器常使用更丰富的System Fω理路System FωSystem F omega · Fω在显式System F中加入kind分类的类型算子、类型级β计算与高阶类型量化。、带类型类或显式强制的核心。Fω不仅让项对普通类型量化，还让类型算子接收类型参数并进行β计算；先用kind判断理路Kind 与类型算子Kind · Type operator · Higher-kinded type用简单kind判断区分完整类型、部分应用的构造器与接收类型算子的高阶算子。区分List与List Int，才能检查这种高阶接口。