System F

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

多态恒等函数

具有类型 $\mathrm{\forall }\alpha .\alpha \to \alpha$，且 $\mathsf{id}[\mathbb{B}]\mathsf{true}{\to }^{\ast }\mathsf{true}$。Church 布尔可赋类型 $\mathrm{\forall }\alpha .\alpha \to \alpha \to \alpha$，自然数可赋类型 $\mathrm{\forall }\alpha .(\alpha \to \alpha )\to \alpha \to \alpha$，显示全称类型能编码数据接口。

边界是把 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ω、带类型类或带显式强制的核心语言上工作。