系统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)
