系統F ，也叫做多態lambda演算 或二階lambda演算 ，是有類型lambda演算 。它由邏輯學家 Jean-Yves Girard 計算機科學家 John C. Reynolds 程式語言 中的參數多態 的概念。
正如同lambda演算 有取值於（range over）函數的變量，和來自它們的粘合子（binder）；二階lambda演算取值自類型 ，和來自它們的粘合子。
作為一個例子，恆等函數有形如A→ A的任何類型的事實可以在系統F中被形式化為判斷
⊢
Λ
α
.
λ
x
α
.
x
:
∀
α
.
α
→
α
{\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }
這裏的α是類型變量
在Curry-Howard同構 下，系統F對應於二階邏輯 。
系統F，和甚至更加有表達力的lambda演算一起，可被看作Lambda立方體 的一部分。
布爾類型被定義為：
∀
α
.
α
→
α
→
α
{\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }
類型變量 。這產生了下列對布爾值TRUE 和FALSE 的兩個定義：
TRUE :=
Λ
α
.
λ
x
α
λ
y
α
.
x
{\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.x}
FALSE :=
Λ
α
.
λ
x
α
λ
y
α
.
y
{\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.y}
接着，通過這兩個λ-項，我們可以定義一些邏輯算子：
AND :=
λ
x
B
o
o
l
e
a
n
λ
y
B
o
o
l
e
a
n
.
(
(
x
(
B
o
o
l
e
a
n
)
)
y
)
F
A
L
S
E
{\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))y)FALSE}
OR :=
λ
x
B
o
o
l
e
a
n
λ
y
B
o
o
l
e
a
n
.
(
(
x
(
B
o
o
l
e
a
n
)
)
T
R
U
E
)
y
{\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))TRUE)y}
NOT :=
λ
x
B
o
o
l
e
a
n
.
(
(
x
(
B
o
o
l
e
a
n
)
)
F
A
L
S
E
)
T
R
U
E
{\displaystyle \lambda x^{Boolean}.((x(Boolean))FALSE)TRUE}
實際上不需要IFTHENELSE 函數，因為你可以只使用原始布爾類型的項作為判定（decision）函數。但是如果需要一個的話：
IFTHENELSE :=
Λ
α
.
λ
x
B
o
o
l
e
a
n
λ
y
α
λ
z
α
.
(
(
x
(
α
)
)
y
)
z
{\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允許以同Martin-Löf類型論 有關的自然的方式嵌入遞歸構造。抽象結構（S）是使用構造子 建立的。有函數被定類型為：
K
1
→
K
2
→
⋯
→
S
{\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}
當
S
{\displaystyle S}
K
i
{\displaystyle K_{i}}
m
{\displaystyle m}
S
{\displaystyle S}
∀
α
.
(
K
1
1
[
α
/
S
]
→
⋯
→
α
)
⋯
→
(
K
1
m
[
α
/
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 }
例如，自然數可以被定義為使用構造子的歸納數據類型
N
{\displaystyle N}
z
e
r
o
:
N
{\displaystyle {\mathit {zero}}:\mathrm {N} }
s
u
c
c
:
N
→
N
{\displaystyle {\mathit {succ}}:\mathrm {N} \to \mathrm {N} }
對應於這個結構的系統F類型是
∀
α
.
α
→
(
α
→
α
)
→
α
{\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }
邱奇數 構成，前幾個是：
0 :=
Λ
α
.
λ
x
α
.
λ
f
α
→
α
.
x
{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x}
1 :=
Λ
α
.
λ
x
α
.
λ
f
α
→
α
.
f
x
{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx}
2 :=
Λ
α
.
λ
x
α
.
λ
f
α
→
α
.
f
(
f
x
)
{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)}
3 :=
Λ
α
.
λ
x
α
.
λ
f
α
→
α
.
f
(
f
(
f
x
)
)
{\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 }
n
{\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
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] （頁面存檔備份 ，存於互聯網檔案館 ）
![{\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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/c8282f31aa836c15fc19cd221479e4a0f775e082)
