系统F ，也叫做多态 lambda 演算 或二阶 lambda 演算 ，是有类型 lambda 演算 。它由逻辑学家 Jean-Yves Girard 和计算机科学家 John C. Reynolds 独立发现的。系统F 形式化了编程语言 中的参数多态 的概念。
正如同 lambda 演算 有取值于(rang 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/zhwiki/api/rest_v1/media/math/render/svg/c8282f31aa836c15fc19cd221479e4a0f775e082)
