System F

定义

System F，又称多态 λ 演算（polymorphic lambda calculus）或二阶 λ 演算，由逻辑学家 Jean-Yves Girard 与计算机科学家 John Reynolds 在二十世纪七十年代各自独立提出。它在简单类型 λ 演算之上增加了对类型的抽象与应用，即全称类型 ∀X.T。

表达能力

System F 可以直接编码自然数、布尔值、列表等数据结构（Church 编码），并且所有良类型程序都强规范化（必然终止）。与 Hindley-Milner 不同，System F 的完整类型推断是不可判定的，因此实际语言多采用其受限片段或要求显式标注。

扩展

System F 加上类型算子得到 System F-omega；GHC Haskell 的核心中间语言即基于 System F 的扩展变体。

意义

System F 是参数化多态（泛型）的标准理论模型，Reynolds 由此发展出的参数性（parametricity）理论解释了「从类型可免费推出定理」的现象。