系统F

系统F，也叫做多态 lambda 演算或二阶 lambda 演算，是有类型 lambda 演算。它由逻辑学家 Jean-Yves Girard 和计算机科学家 John C. Reynolds 独立发现的。系统F 形式化了编程语言中的参数多态的概念。

正如同 lambda 演算有取值于（rang over）函数的变量，和来自它们的粘合子（binder）；二阶 lambda 演算取值自类型，和来自它们的粘合子。

作为一个例子，恒等函数有形如 A→ A 的任何类型的事实可以在系统F 中被形式化为判断

$\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha$

这里的 α 是类型变量。

在 Curry-Howard同构下，系统F 对应于二阶逻辑。

系统F，和甚至更加有表达力的 lambda 演算一起，可被看作 Lambda立方体的一部分。

逻辑和谓词

布尔类型被定义为: $\forall\alpha.\alpha \to \alpha \to \alpha$，这里的 α 是类型变量。这产生了下列对布尔值 TRUE 和 FALSE的两个定义:

TRUE := $\Lambda \alpha.\lambda x^\alpha \lambda y^\alpha.x$

FALSE := $\Lambda \alpha.\lambda x^\alpha \lambda y^\alpha.y$

接着，通过这两个 λ-项，我们可以定义一些逻辑算子:

AND := $\lambda x^{Boolean} \lambda y^{Boolean}.((x (Boolean)) y) FALSE$

OR := $\lambda x^{Boolean} \lambda y^{Boolean}.((x (Boolean)) TRUE) y$

NOT := $\lambda x^{Boolean}. ((x (Boolean)) FALSE) TRUE$

实际上不需要 IFTHENELSE 函数，因为你可以只使用原始布尔类型的项作为判定(decision)函数。但是如果需要一个的话:

IFTHENELSE := $\Lambda \alpha.\lambda x^{Boolean}\lambda y^{\alpha}\lambda z^{\alpha}.((x (\alpha)) y) z$

谓词是返回布尔值的函数。最基本的谓词是 ISZERO，它返回 TRUE 当且仅当它的参数是邱奇数 0:

ISZERO := λ n. n (λ x. FALSE) TRUE

系统F 结构

系统F 允许以同Martin-Löf 类型论有关的自然的方式嵌入递归构造。抽象结构(S)是使用构造子建立的。有函数被定类型为:

$K_1\rightarrow K_2\rightarrow\dots\rightarrow S$

当 $S$ 自身出现类型 $K_i$ 中的一个内的时候递归就出现了。如果你有 $m$ 个这种构造子，你可以定义 $S$ 为:

$\forall \alpha.(K_1^1[\alpha/S]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[\alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha$

例如，自然数可以被定义为使用构造子的归纳数据类型 $N$

$\mathit{zero} : \mathrm{N}$

$\mathit{succ} : \mathrm{N} \to \mathrm{N}$

对应于这个结构的系统F 类型是 $\forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha$。这个类型的项由有类型版本的邱奇数构成，前几个是:

0 := $\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . x$

1 := $\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f x$

2 := $\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f x)$

3 := $\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x))$

如果我们反转 curried 参数的次序(比如 $\forall \alpha. (\alpha \to \alpha) \to \alpha \to \alpha$)，则 $n$ 的邱奇数是接受函数 f 作为参数并返回 f 的 n 次幂的函数。就是说，邱奇数是一个高阶函数 -- 它接受一个单一参数函数 f，并返回另一个单一参数函数。

用在编程语言中

本文用的系统F 版本是显式类型的，或邱奇风格的演算。包含在λ-项内的类型信息使类型检查直接了当。 Joe Wells (1994) 设立了一个"难为人的公开问题"，证明系统 F 的Curry-风格的变体是不可判定的，它缺乏明显的类型提示。[1] [2]

Wells 的结果暗含着系统F 的类型推论是不可能的。一个限制版本的系统F 叫做 "Hindley-Milner"，或简称 "HM"，有一个容易的类型推论算法，并用于了很多强类型的函数式编程语言，比如 Haskell 和 ML。

引用

• Girard, Lafont and Taylor, 1997. Proofs and Types. Cambridge University Press.
• J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176-185, 1994. [3]

外部链接

• Summary of System F by Franck Binard.