十分钟搞懂 Hindley-Milner 类型系统

25/11/2021

类型推理
Let多态
值限制
量词的位置？

❖类型推理

❖什么是类型推理

程序员是懒惰的生物。很多时候，我们并不想啰嗦地给出类型：

1let t = 1 + 1
2let f x = x + 1

这里的 t、f、x 三个变量，每个的类型都是很明确的。当然，更多的时候，显示地给出类型是更好的。

还有一些时候，给出类型并不是很容易的事情，例如：

1let s f g x = f x (g x)
2let k x y = x
3let i = s k k
4let ϕ = s (k (s i)) k

请问，ϕ 的类型是什么？

ϕ 的类型是可以计算出来的，但是非常麻烦。自然的想法是找到一个算法，让计算机代替人脑计算。

事实上，把这段代码送到 haskell 或者 f# 的 repl 里，他们会告诉你ϕ的类型是p -> (p -> q) -> q. 而他们所采用的算法，就是 Hindley-Milner 类型推理算法。

❖类型推理算法

一言以蔽之，类型推理算法就是解方程。方程的建立过程如下：

每个函数的参数，以及每次函数调用的返回值用一个类型变量xᵢ表示。
在函数调用的时候建立方程。f x这个函数调用可以用以下的规则建立方程：

\frac{f:a \rightarrow b\quad x:t_1 \quad (f\ x):t_2}{t_1 \rightarrow t_2 = a \rightarrow b}

例如，这样的函数：

1let f a b = a + b

就可以建立这样的方程：

\begin{aligned} a:\ &t_1 \\ b:\ &t_2 \\ f:\ &t_3 \\ a + b:\ &t_4 \\ (+):\ & \mathsf{int} \rightarrow \mathsf{int} \rightarrow \mathsf{int} \\ t_1 \rightarrow t_2 \rightarrow t₄ =&\ \mathsf{int} \rightarrow \mathsf{int} \rightarrow \mathsf{int} \\ t_3 =&\ t_1 \rightarrow t_2 \rightarrow t_4 \end{aligned}

通过解下面的两个方程，就可以得到每个变量的类型了。现在的问题是，如何解这样的方程呢？

❖Unification

unification是来自于自动定理证明的算法，它可以用来解上述的方程。它背后有一系列关于替换的理论。篇幅所限，我们不会在这里讨论这些理论，而是用很短的篇幅来介绍最自然的算法¹。

首先，上面的方程最多会有两种形式的项参与。一种是类型变量xᵢ，一种是箭头xᵢ → xⱼ. 事实上，箭头xᵢ→ xⱼ可以看作f(xᵢ, xⱼ)，这样我们就有两种形式：

类型变量。
f(v₀, v₁, v₂, ...)的形式。上面的int可以看作int()

算法如下：

遍历每一个方程：

进行自环检查，如果两边出现了
$x_i = \cdots x_i \cdots$
（例如 $x_i = f(x_i)$ ）的形式，那么算法失败。
如果方程的形式为:
$\begin{aligned} x_i &= \star \\ \star &= x_i \end{aligned}$
那么无论 $\star$ 是什么，都用 $\star$ 替换掉还没有遍历过的方程中的 $x_i$
如果不是情况1.，即
$f(x_0, x_1, x_2, \cdots) = g(y_0, y_1, y_2, \cdots)$
那么，
- 如果 $f ≠ g$ ，算法失败。
- 如果 $f = g$ ，加入 $n$ （ $n$ 为 f 的参数个数）个新的待遍历方程 $x_i = y_i$ .

❖Let多态

现在我们已经有了一个类型推理算法。考虑这样的函数：

1let f x = x

上面的推理算法会推出f:x₀ → x₀，这里有一个自由变量 x₀. 采用 System F 的类型记法，对这样的函数进行“泛化”：

\frac{f:\psi(x_0)}{f:\forall x_0.\psi(x₀)}

这样一来，f 的类型就成了“多态类型”，可以进行“例化”：

\frac{f:\forall x.\psi(x)}{f:\psi(a)}

一个麻烦的问题是：在什么时候进行泛化和例化呢？

自然的想法是，在 fun x -> ... 这样的 lambda 表达式外部进行泛化，在引用一个泛化过的变量的时候进行例化。E.g.

1// 以下都是类型正确的项
2(λ x. x) 10
3(λ x. x) true

这样带来的问题是，只有 λ 表达式可以是“多态类型”的，在 lambda 内部的变量仍然只能是单一类型的。

1(λf.(λ t. f true)(f 0))(λx.x)

以上面的表达式为例，即使 λx.x 是多态类型，f 也不能被推理为多态类型。实际上，f在f 0被推理为int → x₀，在f true被推理为bool → x₀. 这样会产生类型错误。

回忆一下，在F#或者ocaml中，f真正被赋予泛型的方法是：

1let f x = x in
2    let t = f 0 in f true

在无类型或简单类型λ表达式中，上面的两段代码完全等价，let只是语法糖。但是在ML系语言中，let却不是语法糖。事实上，ML系语言中，进行“泛化”的时机恰恰是在let绑定这里！

也就是说：

在表达式let var = e₁ in e₂中，e₁的类型被泛化。泛化方法为：
- 当前环境 $Γ$ 中的自由变量为 $F(Γ)$
- $e_1$ 的自由变量为 $F(e_1)$
- 遍历每一个在 $F(e_1) - F(Γ)$ 的自由变量 $x_i$ ， $e_1:t$ 变为 $e_1:∀x_i.t$
每当从当前环境 $Γ$ 中引用一个泛型变量 $e:t_1$ 时，用一个新的类型变量例化 $e:t_1$ 直到 $t_1$ 不再含有 $∀$

而这就是 Hindley-Milner 算法的基本思想。至于具体实现则有algorithm J和algorithm W，请参考维基百科或者 Milner 的原始论文。我的实现采用了alogrithm J.

❖值限制

如果你真的试了之前的代码：

1let s f g x = f x (g x)
2let k x y = x
3let i = s k k
4let ϕ = s (k (s i)) k

你会发现，在Haskell中，这是没问题的：

但是在F#中，这会报错：

为什么要报错呢？这就要从一个更加tricky的程序说起。F#中有可变类型：

1let mutable x = 10
2x <- 20
3printfn "%A" x

如果给出这样的程序：

1let mutable x = []
2x <- [3]
3List.map (fun x -> x = true) x

那么第一行会报错。但是，假设第一行不报错，第二行会不会报错呢？我们要仔细研究一下。

首先，<-的类型虽然F#被隐去了，但是F#有一套已经弃用的操作符!、:=和ref，它们的类型是：

1ref  : 'a -> 'a ref
2(!)  : 'a ref -> 'a
3(:=) : 'a ref -> 'a -> unit

上面的程序写作：

1let x = ref []
2x := [3]
3List.map (fun x -> x = true) x

在第二行被引用的时候，x的类型是't list ref，也就是∀t.ref[list[t]]，它应该被例化为ref[list[b]]，这样一来得到两个等式：

\begin{aligned} \mathsf{ref}[\mathsf{list}[b]] =& \mathsf{ref}[a] \\ a =& \mathsf{list}[\mathsf{int}] \end{aligned}

上面的方程得到 $b = \mathsf{int}, a = \mathsf{list}[\mathsf{int}]$ ，这是不会报错的。而且更大的问题是，在第二行的类型检查之后，b确实变成了int，但这只是 例化的 x，而 $Γ$ 中的x，类型一直都是't list ref，也就是说，第三行照样不会报错！

这就非常糟糕了，因为它引入了类型系统的 unsound. 第三行毫无疑问会出现运行时错误。

为了解决这个问题，ANDREW K. WRIGHT²引入了值限制 (value restriction)。值限制的含义很简单：仅当let var = e₁ in e₂的e₁是语法值(syntactic value)的时候，泛化e₁。如果e₁不是语法值，且他具有不在 $\Gamma$ 中的自由变量，那么报错。

语法值，在ML系语言中就是常量、变量、λ表达式、类型构造器。当然，一个ref[a]类型的值不能被视为语法值。这样一来问题显然已经解决了，因为上面的错误本质上是因为副作用的出现，而对一个语法值求值，在ML中不可能出现副作用。

这个解决方案是过近似的，很多正确的程序（比如之前提到的的程序）也会被拒绝。Haskell由于没有副作用，自然也就不存在这个问题。这也是Haskell能够大量的使用类似于f . g的函数组合，而ML中不能的一大原因。

❖量词的位置？

在 System F 中，量词可以出现在一个类型的任意位置。比如 $∀x.(x → ∀y.y)$ . 事实上，System F 虽然无法构造 Y 组合子（有悖于强规范性），但却可以编码类似于无类型 lambda 演算的 $(x x)$ 结构：

λ(x:∀α.α→α).(x (∀α.α→α))x

这个λ表达式的类型是 $(∀α.α→α)→(∀α.α→α)$ . 它第一个参数的类型决定了它只能作用于Λα.λ(x:α).x这个id函数。把它作用到id的形式用无类型λ表达式写出来就是：

(λx.xx)(λx.x)

毫无疑问它会被β规约为 $λx.x$ .

由此可见，System F中λ表达式，其参数的类型可以含有“多态类型”。那么为什么之前我们的类型推理算法没法推理出它的多态类型呢？

这是因为，之前我们的推理算法可以看作是“简单类型λ表达式”的类型推理算法。而HM类型系统则是简单类型λ表达式的扩展。

说到这里，自然会产生一个疑问：System F 可不可以进行类似的推理呢？或者说，我们这样写：

λ(x:t_1).(x\ t_2)x

有没有一个算法，可以得到通过这个表达式得到 $t_1$ 和 $t_2$ 的值呢？

1985年，Hans-J. Boehm的论文 PARTIAL POLYMORPHIC TYPE INFERENCE IS UNDECIDABLE 告诉我们，如果加入fix组合子，那么上面的问题是不可判定的。1995年，J.B.Wells的论文 Typability and type checking in System F are equivalent and undecidable 进一步告诉我们，如果不给出显式的 $t₁$ 和 $t₂$ ，只要求检查最后的类型，那么这个问题还是不可判定的。

所以，HM 类型系统可以被看成两种 λ 表达式的变种：

如果看成简单类型 λ 表达式的变种，那么HM类型系统加入了let var = e₁ in e₂这种形式，并且允许e₁泛化，实现了参数多态。
如果看成System F的变种，那么HM类型系统限制了量词的位置–只能在类型的最前面。这个限制使得HM类型系统可以实现推理，而 System F 无法实现类型推理。

不过，这并不是说，更强的类型系统就不能进行类型推理了。事实上，Haskell 实现了更强的类型推理，而像 Scala、Typescript、Rust 等语言使用的是一种称作局部类型推理（local type inference）的技术，它在程序员给出一些类型标记的基础上，可以消除大部分不必要的类型标记。