系统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 结构

System F allows recursive constructions to be embedded in a natural manner, related to that in Martin-Löf's type theory. Abstract structures (S) are created using constructors. These are functions typed as:

$K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S$.

Recursivity is manifested when $S$ itself appears within one of the types $K_{i}$. If you have $m$ of these constructors, you can define the type of $S$ as:

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

For instance, the natural numbers can be defined as an inductive datatype $N$ with constructors

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

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

The System F type corresponding to this structure is $\forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha$. The terms of this type comprise a typed version of the Church numerals, the first few of which are:

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

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

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

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

If we reverse the order of the curried arguments (i.e., $\forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha$), then the Church numeral for $n$ is a function that takes a function f as argument and returns the $n^{\textrm {th}}$ power of f. That is to say, a Church numeral is a higher-order function -- it takes a single-argument function f, and returns another single-argument function.

用在编程语言中

The version of System F used in this article is as an explicitly-typed, or Church-style, calculus. The typing information contained in λ-terms makes type-checking straightforward. Joe Wells (1994) settled an "embarrassing open problem" by proving that type checking is undecidable for a Curry-style variant of System F, that is, one that lacks explicit typing annotations. [1] [2]

Wells' result implies that type inference for System F is impossible. A restriction of System F known as "Hindley-Milner", or simply "HM", does have an easy type inference algorithm and is used for many strongly typed functional programming languages such as Haskell and 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.