Hindley-Milner类型系统（2）

类型系统 Haskell

---

类型规则

在关于类型系统的大量文献里，都采用了一种来自于自然推演（Natural Deduction）的符号系统来定义类型系统。HM类型系统的规则定义也不例外。为了能够更好的理解后续的内容，我们先来简单介绍一下这套符号系统。

首先，所有的规则都是基于这样的模式：

$\newcommand{\typerule}[3]{\cfrac{#1}{#2}\scriptstyle{\mathrm{#3}}\displaystyle}$

$$\typerule{J_{1},J_{2}\ldots,J_{n}}{J}{NAME}$$

在右边的NAME是这条规则的名字，可有可无。在线的上方，描述的是前提（premise），前提可以由多个判断（Judgement）组成；在线的下面，给出的是结论（conclusion），结论只能包含一个判断。

因而，这种定义可以理解为：

$$\typerule{\textbf{If these are true}}{\textbf{Then this is true}}{}$$

变量查找

现在我们来看第一个规则：

$$\begin{equation*} \typerule{x:\sigma \in \Gamma}{\Gamma \vdash x:\sigma}{VAR} \end{equation*}$$

这条规则的名字叫做VAR，表示这是一条变量规则。其中 $x:\sigma$ 代表：$x$的类型为$\sigma$；$\Gamma$ 代表已知的事实，在这里可以理解为全局环境。而符号 $\vdash$ 的意思是：可以推导出。

因而，这条规则的意思是：如果一个类型为 $\sigma$ 的变量 $x$ 存在于环境 $\Gamma$ 中；我们则可以从环境 $\Gamma$ 得知 $x$ 的类型是 $\sigma$。

注意这个规则里出现的类型都是$\sigma$，这就意味着存在于环境里的变量，即可能是个monotype，也可能是个polytype。

函数定义

下面我们来看第二条规则：

$$\begin{equation*} \typerule{\Gamma, x:\tau \vdash e:\tau'}{\Gamma \vdash \lambda x.e:\tau \rightarrow \tau '}{ABS} \end{equation*}$$

ABS代表的意思是Abstraction，即Lambda抽象。这里需要介绍一种新语义：在$\Gamma,\Gamma' \vdash e$里，由已知事实 $\Gamma$，加上一个新假设的事实 $\Gamma'$，可以推导出 $e$。如果回到环境的角度，则 $\Gamma$ 代表全局环境，而 $\Gamma'$ 则代表本地环境，它们合在一起，构成一个新环境，从它可以推导出$e$。

所以，第二条规则的意思是：假如允许我们引入一个新的、类型为 $\tau$ 的变量 $x$，从而就可以推导出 $e$ 的类型为 $\tau'$，那我们就可以知道：从现有环境 $\Gamma$ 可以推导出 $\lambda x.e$ 的类型为 $\tau \rightarrow \tau'$。

函数调用

第三条规则用来描述函数调用（Function Application），定义如下：

$$\begin{equation*} \typerule{\Gamma \vdash e_{0}:\tau \rightarrow \tau' \ \ \ \ \ \ \Gamma \vdash e_{1}:\tau}{\Gamma \vdash e_{0}\ e_{1}:\tau'}{APP} \end{equation*}$$

意思很简单：如果由现有环境可以推出$e_{0}$的类型为$\tau \rightarrow \tau'$，$e_{1}$ 的类型为 $\tau$，那么我们就能推出：$e_{0}\ e_{1}$的类型为$\tau'$。

规则二和规则三，是对偶关系，分别定义函数和函数调用相关的类型规则。与这两条规则有关的类型全是$\tau$，即monotype。这就意味着，在HM类型系统里，lambda的参数和结果，都只能是monotype。

对于形如 $\forall a\ b. (a \rightarrow b) \rightarrow a \rightarrow b$ 的类型，如果我们将其看作一个 $\lambda$ 函数，就会知道，在一次实例化的过程中，其参数 $a,b,c$ 都只能各自被实例化为一种类型。比如：

$$\begin{align*} & \big (\forall a\ b. (a \rightarrow b) \rightarrow a \rightarrow b)\big)\ \textbf{Int Bool} \\ \Rightarrow \ & (\textbf{Int} \rightarrow \textbf{Bool}) \rightarrow \textbf{Int} \rightarrow \textbf{Bool} \end{align*}$$

而对于 $\forall a\ b. (\forall c. c \rightarrow c) \rightarrow (a, b) \rightarrow (a,b)$ 这样类型的函数，我们在一个上下文里对 $a,b$ 进行实例化后，得到的类型里 $\forall c. c \rightarrow c$ 依然还是个多态类型。

$$\begin{align*} & \big (\forall a\ b. (\forall c. c \rightarrow c) \rightarrow (a, b) \rightarrow (a,b) \big) \textbf{Int Bool} \\ \Rightarrow \ & (\forall c. c \rightarrow c) \rightarrow (\textbf{Int, Bool}) \rightarrow (\textbf{Int, Bool}) \end{align*}$$

这就像$\lambda$演算里的高阶函数一样，这种类型被称为类型系统里的高阶类型（higher rank type）。

因而，我们可以在同一个上下文里，对这个高阶类型进行多次不同的实例化。比如如下代码，在对高阶类型支持的类型系统下是可以通过检查和编译的。

g :: forall a b. (forall c. c -> c) -> (a, b) -> (a, b)
g f (x,y) =  (f x, f y)

但正如我们之前所提到的，在HM类型系统里，所有的 $\forall$ 都必须出现在最前面，这也就意味着不允许存在高阶类型。因而函数 $g$ 的类型在HM类型系统下非法。

Let Binding

我们重新回到类型规则，来看看第四条：

$$\begin{equation*} \typerule{\Gamma \vdash e_{0}:\sigma \ \ \ \ \ \ \Gamma,x:\sigma \vdash e_{1}:\tau}{\Gamma \vdash \mathbf{let}\ x= e_{0}\ \mathbf{in}\ e_{1}:\tau}{LET} \end{equation*}$$

这条规则被称做Let Binding，其意思是：如果由现有环境可以推论出$e_{0}$的类型是$\sigma$；同时，如果引入一个类型同样为$\sigma$的临时变量$x$，则可以由现有环境推论出$e_{1}$的类型为一个单态类型$\tau$；那么，我们就可以推论出：表达式$\textbf{let }x=e_{0} \textbf{ in } e_{1}$的类型为单态类型$\tau$。

从语义上，这条规则似乎没有什么难以理解的。并且，它貌似可以通过ABS和APP两条规则组合而来。毕竟，在$\lambda$算子理论里，$\textbf{let }x=e_{0} \textbf{ in } e_{1}$等价于$(\lambda x.e_{1})\ e_{0}$。

但是，这条规则正是HM类型系统最为特别的地方：由于$\lambda$定义本身不允许高阶类型，因而如下代码完全无法通过类型系统的检查：

(\x -> x x) (\x -> x)

但是，在不引入高阶类型的前提下，Let Binding却可以让上面等价语义的代码通过类型检查，如下：

let f = \x -> x in f f

在这个表达式里，$\mathbf{f}$的类型为$\forall \alpha. \alpha \rightarrow \alpha$，正如LET规则所描述的，这是个$\sigma$所允许的多态类型。在$f\ f$表达式里，$f$的两次出现，其类型都是多态类型，因而可以各自实例化：

$$\begin{align*} \textbf{f}_{1st}: &\ \ (\forall \alpha. \alpha \rightarrow \alpha)\ (\beta \rightarrow \beta)\ \ \ \ & \Rightarrow & \ \ \ \ (\beta \rightarrow \beta) \rightarrow (\beta \rightarrow \beta) \\ \textbf{f}_{2nd}: &\ \ (\forall \alpha. \alpha \rightarrow \alpha)\ \beta \ \ \ \ & \Rightarrow & \ \ \ \ \beta \rightarrow \beta \end{align*}$$

因而，在HM类型系统里，尽管let binding和$\lambda$定义依然具备等价的替换（substitution）语义，但是在类型的宽容度上，两者已经不再等价。所以，在HM类型系统下，let binding不仅仅是一个$\lambda$的语法糖，它提供了更强大的能力。而这种能力被称做LET绑定时多态（let polymorphism）。

$\lambda$的单态与多态

在HM类型系统下，所有的$\lambda$的类型都是monotype。因而当看到如下定义时，我们必须清楚：等号右边的$\lambda$表达式的类型是$a\rightarrow a$，即没有前面的$\forall$，因而它是monotype。

你一定会质疑：明明类型标注上的$\forall$写的清清楚楚！

没错，但那不是等号右边$\lambda$表达式的类型，而是等号左边的变量id的类型。在HM类型系统下，将monotype转为polytype的唯一方式就是通过LET绑定时多态，即通过等号进行变量绑定时。haskell的顶层，不过是一个隐形的大let语句。

id :: forall a. a -> a
id = \x -> x

事实上，等号右边的$\lambda$完全没有任何理由属于polytype。因为，对于一个$\lambda$定义，如果不将其绑定到任何变量，那么它将只能使用一次，只有变量才让它具备多次被使用的可能性。只需要使用一次，意味着它只可能有一种类型，并不存在多次实例化的需要。

为了更清晰的理解这一点，我们来假设HM类型系统并不支持LET绑定时多态，这种情况下，我们用下面的表达式，与注释里在支持LET绑定时多态情况下的let表达式等价：

(\x -> x) (\x -> x) -- 等价于：let f = \x -> x in f f 

这是因为，我们将同一个$\lambda$定义实现了两次。虽然它们的定义看起来一摸一样，但在类型系统的眼里，它们是两个独立的$\lambda$，因而会各自推演它们的类型。并且也确实各自推演出了不同的类型。

因而，站在$\lambda$的外部来看，$\lambda$的类型没有任何理由属于polytype。

但是，站在$\lambda$的内部，当它使用一个函数类型的参数时（当然，参数是一个名字），是否支持其参数绑定时多态，将会产生重大的不同。

比如，如下代码里，参数$g$被实例化为不同的类型。而这只有在允许参数绑定时多态的情况下，那行表达式才能通过类型系统的检查。而一旦支持了参数绑定时多态，那么函数$f'$的实现里，虽然传入的是一个$\lambda$（我们之前刚刚讨论过，$\lambda$的类型必然是monotype），但其与函数 $f$ 的参数 $g$ 进行绑定的过程中，类型会自动升级为polytype。

f :: (forall a. a -> a) -> (Bool, Int)
f = \g -> (g True, g Int)
f' = f (\x -> x)

而参数绑定时多态，被称做higher rank type。为了支持这种能力，需要程序员给出类型注解。这就违背了HM类型系统设计的初衷。因为HM类型系统的本意，正是在完全不需要程序员给出类型注解的前提下，可以完全推断出所有表达式的类型。

类型泛化

第五条规则被称做泛化（Generalization），定义如下：

$$\begin{equation*} \typerule{\Gamma \vdash e:\sigma \ \ \ \ \alpha \notin free(\Gamma)}{\Gamma \vdash e:\forall \alpha.\sigma}{GEN} \end{equation*}$$

自由与边界

为了进一步理解polytype里的类型变量，让我们再次回到$\lambda$的世界。

在$\lambda$表达式里，变量一共分为两类：

1. 自由变量（Free Variable）
2. 有界变量（Bound Variable）

比如，表达式$\lambda x. x + y$的子表达式$x+y$里，$x$就是有界变量，因为$\lambda$有个同名参数$x$，因而它被约束在$\lambda$的范围内；而$y$由于没有任何参数可以绑定，被称作自由变量。

一个表达式里，只有自由变量可以被替换。比如，当我们试图对表达式$\lambda x. x + y$执行替换操作$[x \mapsto 10, y \mapsto 3]$，我们得到的结果是$\lambda x. x + 3$，只有自由变量 $y$ 发生了替换，而有界变量 $x$ 未受影响。

而在同一个表达式里，同一个名字的变量，即可能是自由的，也可能是有界的。这是因为它们虽然都是同一个名字，但事实上代表着不同的变量。比如：$x + (\lambda x.x + y)\ z$里，第一个$x$是一个自由变量，第二个是参数，第三个$x$则是一个有界变量，$y$和$z$也都是自由变量。

如果我们对这个表达式执行替换操作$[x \mapsto 10, y \mapsto 3, z \mapsto 5]$ ，得到的结果是：$10 + (\lambda x.x + 3)\ 5$。

现在回到类型的世界。

既然$\forall$是类型系统里的$\lambda$，同样的道理，对于$\forall \alpha. \alpha \rightarrow \beta$这样的类型，$\alpha$是一个有界类型变量，而$\beta$则属于自由类型变量。

如果对整个类型执行替换操作$[\alpha\mapsto\textbf{Int},\beta\mapsto\textbf{Bool}]$，得到的结果是$\forall \alpha. \alpha \rightarrow\textbf{Bool}$。

而对于表达式$\alpha \rightarrow \beta$，$\alpha$和$\beta$都是自由类型变量。如果对整个类型执行替换操作$[\alpha\mapsto\textbf{Int},\beta\mapsto\textbf{Bool}]$，得到结果是$\textbf{Int}\rightarrow\textbf{Bool}$。

需要强调的是：从$\sigma$的定义可以看出，在HM类型系统里，如果一个类型属于polytype，其所有的$\forall$都只能出现在最前面。

也就是说，我们只能定义形如$\forall\alpha.\forall \beta. \alpha \rightarrow \beta$这样的polytype，而不可能定义$\forall \alpha. \alpha \rightarrow (\forall \beta. \beta \rightarrow \alpha) \rightarrow \alpha$这样的polytype。

函数$\mathbf{free}(x)$则是用来求$x$所拥有的所有自由类型变量，其结果是一个集合。

比如：$\mathbf{free}(\lambda \alpha. \alpha \rightarrow \beta \rightarrow \gamma) = \{\beta,\gamma\}$；而$\mathbf{free}(\alpha \rightarrow \beta) = \{\alpha,\beta\}$。

环境$\Gamma$里，存储的是所有已知的$x:\sigma$的集合。因而，

$$\begin{align*} \mathbf{free}(\Gamma) = \displaystyle\bigcup_{x:\sigma \in \Gamma}\mathbf{free}(\sigma) \end{align*}$$

代表现有环境中所有的自由类型变量的集合。

它的意思是：如果由现有环境可以推导出表达式$e$的类型为$\sigma$，对于$\sigma$里的任意自由变量，如果不存在于 $\mathbf{free}(\Gamma)$，那么它就可以成为 $\sigma$ 的 $\forall$ 参数。

比如，我们基于现有的环境推导出$e$的类型为$\alpha \rightarrow \beta \rightarrow \gamma$，这个类型包含三个自由类型变量: $\alpha, \beta, \gamma$。其中，如果$\beta$是环境中已经存在的自由类型变量，但$\alpha, \gamma$不是，那么上述类型就可以泛化为：$\forall \alpha\ \gamma. \ \alpha \rightarrow \beta \rightarrow \gamma$。

所以，为了更清晰的表述，这条规则可以修正为：

$$\begin{align*} \typerule{\Gamma \vdash e:\sigma \ \ \ \ \overline{\alpha} \neq \phi }{\Gamma \vdash e:\forall \overline\alpha.\sigma}{GEN} \ \ \ \ \ \ \ \ \mathbf{(\overline\alpha = \mathbf{free}(\sigma) - \mathbf{free}(\Gamma))} \end{align*}$$

类型实例化

最后一条规则称做实例化（Instantiation）：

$$\begin{equation*} \typerule{\Gamma \vdash e:\sigma \ \ \ \ \ \sigma \succeq \sigma'}{\Gamma \vdash e:\sigma'}{INST} \end{equation*}$$

这条规则定义里有一个重要的新符号$\succeq$，它表示左边比右边的类型更通用，更泛化，更多态。当然，也可以反过来说，右边比左边的更特殊，更具体。比如:

$$\begin{align*} Int\ \ \ &\succeq \ \ \ Int \\ Int \rightarrow Int\ \ \ &\succeq\ \ \ Int \rightarrow Int \\ \forall \alpha\ \beta.\alpha \rightarrow \beta\ \ \ & \succeq \ \ \ \forall \alpha.\alpha \rightarrow \alpha \\ \forall \alpha\ \beta.\alpha \rightarrow \beta\ \ \ & \succeq \ \ \ \forall \alpha\ \beta.[\alpha] \rightarrow [\alpha] \end{align*}$$

在其它文献中，也有使用符号$\sqsubseteq$或$\leq$的。它们都和$\succeq$一样，代表左边比右边更通用。比如：

$$\begin{align*} \forall \alpha\ \beta.\alpha \rightarrow \beta\ \ \ \sqsubseteq \ \ \ &\forall \alpha.\alpha \rightarrow \alpha \\ \forall \alpha\ \beta.\alpha \rightarrow \beta\ \ \ \leq \ \ \ &\forall \alpha\ \beta.[\alpha] \rightarrow [\beta] \end{align*}$$

但对我个人而言，符号的开口朝向更加通用的类型，更符合我的直觉。因而，本文均采用符号$\succeq$。

理解这个符号之后，这条规则的意思也就呼之欲出：如果从现有环境可以推出表达式$e$的类型为$\sigma$，并且$\sigma$比$\sigma'$更加通用，那么我们就可以从现有环境推出：表达式$e$的类型可以是更加具体的$\sigma'$。

或许你已经注意到，最后两条规则：INST和GEN是一对互逆的规则。一个表达式的类型可以通过GEN提升到更加通用；相反，也可以通过INST降格到更加具体。

小结

本文介绍了HM类型系统的六条类型规则。在随后的文章里会讨论基于这六条规则的类型推导。