简介

在数学 (尤其指数理逻辑分支) 与类型论的世界, Lambda 立方体 是由 Henk Barendregt 提出的一个框架, 用以探索及研究 简单类型 \(\lambda\)-演算 于不同维度上扩展出来对应的 类型系统, 其也阐述了处于不同维度上的 类型系统 中 类型 (Type) 与值 (Term) 的依赖关系 究竟是怎样的, 简单来说我们可以以三种不同方向的箭头 (维度) 定义出不同类型系统之间是怎样扩展开来的.

三种不同的维度分别代表的含义

  • Y轴 (\(\uparrow\)): 值依赖于类型, 可被对应到 多态 (Polymorphism) 的概念
  • X轴 (\(\to\)): 类型依赖于值, 可被对应到 依赖类型 (Dependent types) 的概念
  • Z轴 (\(\nearrow\)): 类型依赖于类型, 可被对应到 类型构造器 (Type operators) 的概念

类型系统

于 Lambda 立方体中, 我们会定义出不同形式的类型系统用以描述各自不同系统之间的作用与规则, 下面将会略举一些例子:

(\(\lambda\to\)) 简单类型 Lambda 演算

简单类型 Lambda 演算是 Lambda 立方体中最为简单的类型系统, 其只能够透过 值依赖于值 (a term depend on a term) 的方式构造出来

类型推导规则

简单类型 Lambda 演算 使用了以下的类型推导规则:

  1. \({\frac { x\ :\ \sigma\ \in\ \Gamma }{ \Gamma\ \vdash\ x\ :\ \sigma }}\)(\(start\ rule\))
    假设上下文 (Typing environment) \(\Gamma\) 中存在 \(x\) 的类型为 \(\sigma\), 则可推导出 \(x\) 的类型为 \(\sigma\) .

  2. \({\frac { \Gamma\ \vdash\ M\ :\ (\sigma\ \to\ \tau)\quad\Gamma\ \vdash\ N\ :\ \sigma }{ \Gamma\ \vdash\ (M\ N)\ :\ \tau }}\)(\(\to-elimination\))
    给定上下文 \(\Gamma\), 其能推导出 \(M\) 的类型为 \(\sigma \to \tau\)\(N\) 的类型为 \(\sigma\), 则可推导出 \(M\ N\) 的类型为 \(\tau\) .

  3. \({\frac { \Gamma\ ,\ x\ :\ \sigma\ \vdash\ M\ :\ \tau }{ \Gamma\ \vdash\ (\lambda x.\ M)\ :\ (\sigma\ \to\ \tau) }}\)(\(\to-introduction\))
    \(\Gamma\) 并且有 \(x\) 的类型为 \(\sigma\) 该两个上下文, 假设 \(\Gamma\) 能够推导出 \(M\) 的类型为 \(\tau\), 则亦可推导出 \(\lambda x. M\) 的类型为 \(\sigma \to \tau\) .

\(\lambda\to_{Curry}\)\(\lambda\to_{Church}\) 的差异

\(\lambda\to_{Curry}\)\(\lambda\to_{Church}\) 这两种系统均能表达 \(\lambda\to\) 的含义, 而上述的推导规则是使用了 \(Curry\) 版本编写的, 而两者的不同点则在于:

  • \(Curry\) 版本的推导规则为: \(\vdash_{Curry} (\lambda x.x) : (\sigma \to \sigma)\)
  • \(Church\) 版本的推导规则为: \(\vdash_{Church} (\lambda x : \sigma .x) : (\sigma \to \sigma)\)

可见一般在 \(Curry\) 中的一个值 \(\lambda x. x\) 将会被 \(Church\) 标记为 \(: \sigma\), 即显式地标记参数 \(x\) 的类型为 \(\sigma\). 由于我们能够显式地标记值上参数的类型, 因此我们就能够根据该参数的类型直接决定 (Decide) 某个值上究竟是什么类型, 而对于某些使用 \(Curry\) 系统定义的规则, 在某些问题上他们是不可决定的 (Undecidable).

(\(\lambda 2\)) 系统 F

系统 F 相较于 简单类型 \(\lambda\) 演算 只能够透过 值依赖于值 的方式去构造出一个抽象 (Abstraction), 其也能够 依赖于类型的值 (terms to depend on types).

类型推导规则

系统 F 使用的推导规则除了包含 简单类型 \(\lambda\) 演算的 \(start\ rule\), \(\to-elimination\) 以及 \(\to-introduction\) 规则外, 额外新增了:

  1. \({\frac { \Gamma\ \vdash\ M\ :\ (\forall\alpha.\ \sigma) }{ \Gamma\ \vdash\ M\ :\ (\sigma[\alpha\ :=\ \tau]) }}\), \(\tau \in \Bbb{T}\) (\(\forall-elimination\))
    给定上下文 \(\Gamma\), 其能推导出 值 \(M\) 有类型 \(\forall\alpha. \sigma\), 则亦可推导出 \(M\) 的类型为 \(\sigma[\alpha := \tau]\) (在这里 \(\tau\) 为实际的类型, \(\alpha\) 为类型参数, 也就是 类型 \(\sigma\) 依赖于 \(\alpha\) 的值, 即 \(\tau\)).

  2. \({\frac { \Gamma\ \vdash\ M\ :\ \sigma }{ \Gamma\ \vdash\ (\Lambda \alpha. M)\ :\ (\forall\alpha.\sigma) }}\),\({\ \alpha \notin FV(\Gamma)}\) (\(\forall-introduction\))
    给定上下文 \(\Gamma\)\(\alpha\) 不是 \(\Gamma\) 的 自由变量, 其能推导出 \(M\) 有类型 \(\sigma\), 则该上下文亦可推导出 \(M\) 有类型 \(\forall\alpha. \sigma\) (值上的 \(\Lambda \alpha\) 可显式指定 \(\alpha\) 的类型).

进一步的扩展规则

除了上述的两条规则外, 由于系统 F, 即 \(\lambda 2\), 与 \(\lambda\mu\) 以及 \(\lambda P\) \((\lambda\cap)\), 均是由 \(\lambda\to\) 延伸出来的, 这些系统都能够加入 \(equality\ rule\ (EQ)\)\(approximation\ rule\ (A)\) 作推导, 亦能够相互组合出诸如 \(\lambda 2\mu\)\(\lambda\mu\cap\) 等更强的系统.

  1. \({\frac { M\ :\ \sigma \quad M\ =_{\beta} \ N }{ N\ :\ \sigma }}\)(\(EQ\))
    设有值 \(M : \sigma\) 且已知 \(M = N\), 则可推导出 \(N\) 的类型为 \(\sigma\) .

  2. \({\frac { \Gamma\ \vdash\ P\ :\ \sigma\ for\ all\ P\ \in\ A(M) }{ \Gamma\ \vdash\ M\ :\ \sigma }}\)(\(A\))

  3. \({\frac {}{ \Gamma\ \vdash\ \bot\ :\ \sigma }}\)(\(A\))

编程上的例子

该规则的定义恰恰对应到了许多编程语言中 多态化参数 (Parametric polymorphism) 的特性, 例如于 Haskell 中 id, const, justInt 以及 intOrStr 的定义实际为:

1
2
3
4
5
6
7
8
9
10
11
id :: forall a. a -> a
id x = x

const :: forall a b. a -> b -> a
const x y = x

justInt :: Maybe Int
justInt = Just 123

intOrStr :: Either Int String
intOrStr = Right "foo"

我们能够透过 forall a.forall a b. 以显式捕获这些函数的多态参数.

而我们可以将上述例子对应到推导的表达式, 正如: \((\Lambda a. \lambda x. x) : (\forall a. a \to a) \vdash_{\lambda 2} (\lambda x. x) : ((a \to a)[a := \tau])\) \((\Lambda a\ b. \lambda x\ y. x) : (\forall a\ b. a \to b \to a) \vdash_{\lambda 2} (\lambda x\ y. x) : ((a \to b \to a)[a := \tau_1, b := \tau_2])\) \((Just\ 123) : (Maybe\ Int) \vdash_{\lambda 2} (Just\ 123) : Maybe[\alpha := Int]\) \((Right\ "foo") : (Either\ Int\ String) \vdash_{\lambda 2} (Right\ "foo") : Either[\alpha := Int, \beta := String]\)

(\(\lambda\underline{\omega}\)) 系统 \(\lambda\underline{\omega}\)

系统 \(\lambda\underline{\omega}\) 相较于 简单类型 \(\lambda\) 演算 只能够透过 值依赖于值 的方式以构造出一个抽象, 其允许了 类型依赖于类型 (types to depend on types) 的情况出现.

Kind (\(*\)) 的引入

由于 \(\lambda\underline{\omega}\) 需要表达出类型依赖于类型的概念, 正如 \(\alpha \to \alpha\) 一样, \(\alpha\) (即函数的协变位置) 依赖于 \(\alpha\) (函数的逆变位置), 因此我们需要引入 \(Kind\), 即 类型的类型 的概念. 例如把一个 \(Kind\) 的表达式定义为 \(\alpha, \beta \in \Bbb{T} \implies (\alpha \to \beta) : \Bbb{T}\), 这里不难看出 \(\alpha, \beta, (\alpha \to \beta) \in \Bbb{T}\), 因此 \(\Bbb{T}\) 亦可被称之为类型的类型, 即 \(Kind\), 形式化地整句表达式可被定义为 \(\alpha : *, \beta : * \vdash (\alpha \to \beta) : *\) (使用 \(\sigma : *\) 取代了 \(\sigma \in \Bbb{T}\)).

Kind 集合 (\(\Bbb{K}\)) 与 \(Kind\) 构造器 (类型构造器)

由于 \(Kind\) 的表达式, 如 \(f \equiv \lambda\alpha : *. \alpha \to \alpha\) 中, \(f\) 既不处于值上, 亦不是居留在类型上, 因此我们需要定义出一个新的集合负责存储起这些 \(kinds\) : \[\Bbb{K} = *\ |\ \Bbb{K} \to \Bbb{K}\] 即有 \(\Bbb{K} = \lbrace *, * \to *, * \to * \to *, ... \rbrace\). 若果 \(\vdash k : \Box\)\(\vdash F : k\) (这里的 \(k : \Box\) 实际上对应了 \(k \in \Bbb{K}\)), 则 \(F\) 被称之为 \(kind\ k\) 的构造器 (类型构造器).

类型推导规则

  1. \(<> \vdash * : \Box\) (\(axiom\)) 空的上下文总能被推导出 \(* : \Box\)

  2. \({\frac{ \Gamma\ \vdash\ A\ :\ s }{ \Gamma,\ x\ :\ A\ \vdash\ x\ :\ A }}\), \(x \notin \Gamma\) (\(start\ rule\))

  3. \({\frac{ \Gamma\ \vdash\ A\ :\ B \quad \Gamma\ \vdash\ C\ :\ s }{ \Gamma,\ x\ :\ C\ \vdash\ A\ :\ B }}\), \(x \notin \Gamma\) (\(weakening\ rule\))

  4. \({\frac{ \Gamma\ \vdash\ A\ :\ s \quad \Gamma\ \vdash\ B\ :\ s }{ \Gamma\ \vdash\ (A\ \to\ B)\ :\ s }}\)(\(type/kind\ formation\))
    这里的 \(formation-rule\) 指的是怎样把某一个 \(kind\) (这里是 \(s\)) 构建成一个类型, 例如这里则是当有 \(A\) 以及 \(B\) 皆为类型时, 则能构筑表达式 \(A \to B\) 是一接受 \(A\) 类型并且返回 \(B\) 类型的函数.

  5. \({\frac{ \Gamma\ \vdash\ F\ :\ (A\ \to\ B) \quad \Gamma\ \vdash\ a\ :\ A }{ \Gamma\ \vdash\ Fa\ :\ B }}\)(\(application\ rule\))

  6. \({\frac{ \Gamma,\ x\ :\ A\ \vdash\ b\ :\ B \quad \Gamma\ \vdash\ (A\ \to\ B)\ :\ s }{ \Gamma\ \vdash\ (\lambda x\ :\ A.\ b)\ :\ (A\ \to\ B) }}\)(\(abstraction\ rule\))

  7. \({\frac{ \Gamma\ \vdash\ A\ :\ B \quad \Gamma\ \vdash\ B'\ :\ s \quad B\ =_{\beta}\ B' }{ \Gamma\ \vdash\ A\ :\ B' }}\)(\(conversion\ rule\))

编程上的例子

于 Haskell 中, 我们得知一个 Functor (f :: * -> *) 其本身是一类型构造器, 现在则可利用 \(\lambda\to\) 以及 \(\lambda\underline{\omega}\) 的规则, 对 fmap (*2) [1..10] (或 (*2) <$> [1..10]) 进行简单的类型推导:

\[ \dfrac { \dfrac { \dfrac { \begin{aligned} \vdots \end{aligned} } { \Gamma, l : [a] \vdash fmap\ (*2) : [b] } \quad \dfrac { \dfrac { \Gamma \vdash [] : (* \to *) \quad \Gamma \vdash a : * } { \Gamma \vdash [a] : * } (\lambda\underline{\omega}\ app.) \quad \dfrac { \Gamma \vdash [] : (* \to *) \quad \Gamma \vdash b : * } { \Gamma \vdash [b] : * } (\lambda\underline{\omega}\ app.) } { \Gamma \vdash ([a] \to [b]) : * } (\lambda\underline{\omega}\ form.) } { \Gamma \vdash \lambda l. fmap\ (*2) : ([a] \to [b]) } (\lambda\underline{\omega}\ abst.) \quad \dfrac { \begin{align} \vdots \\ \end{align} } { \Gamma \vdash [1..10] : [a] } } { \Gamma \vdash fmap\ (*2)\ [1..10] : [b] } (\lambda\to elim.) \]

(\(\lambda P\)) Lambda-P

系统 \(\lambda P\) 相较于 简单类型 \(\lambda\) 演算 只能够透过 值依赖于值 的方式以构造出一个抽象, 亦可于类型上以值作为参数, 正如一个直观的例子 \(A^n \to B\) 阐述了 \(n\) 实际上是一个值 (例如一个自然数), \(A\)\(B\) 是类型, 而我们需要构造 \(B\) 的时候则必须传入一个值, 因此可被描述为 依赖于值的类型 (types to depend on terms).

类型推导规则

系统 \(\lambda P\) 使用了如下规则进行推导 (其中 \(*\)\(\Box\)\(\lambda P\) 表达式中的常量):

  1. \(<>\ \vdash * : \Box\) (\(axiom\)) 空的上下文总能被推导出 \(* : \Box\)

  2. \({\frac { \Gamma\ \vdash\ A\ :\ s }{ \Gamma,\ x\ :\ A\ \vdash\ x\ :\ A }}\), \(x \notin \Gamma\) (\(start\ rule\))

  3. \({\frac { \Gamma\ \vdash\ A\ :\ B \quad \Gamma\ \vdash\ C\ :\ s }{ \Gamma,\ x\ :\ C\ \vdash\ A\ :\ B }}\), \(x \notin \Gamma\) (\(weakening\ rule\))

  4. \({\frac { \Gamma\ \vdash\ A\ :\ * \quad \Gamma,\ x\ :\ A\ \vdash\ B\ :\ s }{ \Gamma\ \vdash\ (\Pi x\ :\ A.\ B)\ :\ s }}\)(\(type/kind\ formation\))

  5. \({\frac{ \Gamma\ \vdash\ F\ :\ (\Pi x\ :\ A.\ B) \quad \Gamma\ \vdash\ a\ :\ A }{ \Gamma\ \vdash\ Fa\ :\ B[x\ :=\ a] }}\)(\(application\ rule\))

  6. \({\frac{ \Gamma,\ x\ :\ A\ \vdash\ b\ :\ B \quad \Gamma\ \vdash\ (\Pi x\ :\ A.\ B)\ :\ s }{ \Gamma\ \vdash\ (\lambda x\ :\ A.\ b)\ :\ (\Pi x\ :\ A.\ B) }}\)(\(abstraction\ rule\))

  7. \({\frac{ \Gamma\ \vdash\ A\ :\ B \quad \Gamma\ \vdash\ B'\ :\ s \quad B\ =_{\beta}\ B' }{ \Gamma\ \vdash\ A\ :\ B' }}\)(\(conversion\ rule\))

(\(\lambda\omega\)) 系统 \(\lambda\omega\)

系统 \(\lambda\omega\) 结合了 \(\lambda 2\)\(\Lambda\) 构造器, \(\lambda\underline{\omega}\) 的 类型构造器 与他们各自的推导规则, 其允许了 依赖于类型的值 (terms to depend on types) 以及 类型依赖于类型 (types to depend on types) 同时存在, 因此从计算的角度来看, 其表达能力非常强, 同时亦被认为具备编程语言所需达到的基础.

(\(\lambda C\)) 系统 \(\lambda C\)

系统 \(\lambda C\) 位于 Lambda 立方 的最右上角, 其包含了来自于 \(\lambda P\) 逻辑谓词的表达能力 与 \(\lambda\omega\) 的计算能力, 因此无论是从逻辑或是计算的角度考量, 均被视为极度具备强大能力的一套类型系统.

与逻辑系统的关系

透过 Curry-Howard 同构, 我们得以将 Lambda 立方体 中的类型系统与逻辑系统一一对应起来, 如下表:

类型系统 逻辑系统
\(\lambda\to\) (一阶) 命题逻辑
\(\lambda 2\) 二阶命题逻辑
\(\lambda\underline{\omega}\) 弱高阶命题逻辑
\(\lambda\omega\) 高阶命题逻辑
\(\lambda P\) 一阶谓词逻辑
\(\lambda P2\) 二阶谓词逻辑
\(\lambda P\underline{\omega}\) 弱高阶谓词逻辑
\(\lambda C\) 构造演算

外部链接

本文部分内容参考或引用至下列网页,也可供作为额外的延伸资源帮助阅读: