系統F

系統F，也叫做多態lambda演算或二階lambda演算，是有類型lambda演算。它由邏輯學家Jean-Yves Girard（英語：Jean-Yves Girard）和計算機科學家John C. Reynolds（英語：John C. Reynolds）獨立發現的。系統F形式化了程式語言中的參數多態的概念。

正如同lambda演算有取值於（range over）函數的變量，和來自它們的粘合子（binder）；二階lambda演算取值自類型，和來自它們的粘合子。

作為一個例子，恆等函數有形如A→ A的任何類型的事實可以在系統F中被形式化為判斷

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

這裏的α是類型變量（英語：type variable）。

在Curry-Howard同構下，系統F對應於二階邏輯。

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

邏輯和謂詞

布爾類型被定義為： ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$，這裏的α是類型變量。這產生了下列對布爾值TRUE和FALSE的兩個定義：

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

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

接着，通過這兩個λ-項，我們可以定義一些邏輯算子：

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

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

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

實際上不需要IFTHENELSE函數，因為你可以只使用原始布爾類型的項作為判定（decision）函數。但是如果需要一個的話：

IFTHENELSE := ${\displaystyle \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）是使用構造子建立的。有函數被定類型為：

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

當${\displaystyle S}$自身出現類型${\displaystyle K_{i}}$中的一個內的時候遞歸就出現了。如果你有${\displaystyle m}$個這種構造子，你可以定義${\displaystyle S}$為：

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

例如，自然數可以被定義為使用構造子的歸納數據類型${\displaystyle N}$

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

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

對應於這個結構的系統F類型是 ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$。這個類型的項由有類型版本的邱奇數構成，前幾個是：

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

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

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

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

如果我們反轉curried參數的次序（比如${\displaystyle \forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha }$），則${\displaystyle 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.