类型推理

什么是类型推理

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

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

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

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

let s f g x = f x (g x)
let k x y = x
let i = s k k
let ϕ = s (k (s i)) k

请问,ϕ的类型是什么?

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

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

类型推理算法

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

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

f:ab,x:t,(fx):ttt=ab\frac{f:a → b, x:t₁, (f x):t₂}{t₁ → t₂ = a → b}

例如,这样的函数:

let f a b = a + b

就可以建立这样的方程:

a:tb:tf:ta+b:t(+):intintintttt=intintintt=ttt\begin{aligned} a:&t₁ \\ b:&t₂ \\ f:&t₃ \\ a + b:&t₄ \\ (+):& int → int → int \\ t₁ → t₂ → t₄ &= int → int → int \\ t₃ &= t₁ → t₂ → t₄ \end{aligned}

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

Unification

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

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

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

算法如下:

遍历每一个方程:

  1. 进行自环检查,如果两边出现了

    x=...x...xᵢ = ...xᵢ...

(例如x=f(x)xᵢ = f(xᵢ))的形式,那么算法失败。
2. 如果方程的形式为:

x==x\begin{aligned} xᵢ &= ⋆ \\ ⋆ &= xᵢ \end{aligned}

那么无论 是什么,都用 替换掉还没有遍历过的方程中的 xxᵢ
3. 如果不是情况1.,即

f(x,x,x,...)=g(y,y,y,...)f(x₀, x₁, x₂,...) = g(y₀, y₁, y₂, ...)

那么,

  • 如果fgf ≠ g,算法失败。
  • 如果f=gf = g,加入nnnn为f的参数个数)个新的待遍历方程x=yxᵢ = yᵢ.

¹文末给出的实现采用的是基于并查集的算法

Let多态

现在我们已经有了一个类型推理算法。不过,我们并没有推出“多态类型”的能力。这似乎并不正确,因为考虑这样的函数:

let f x = x

上面的推理算法会推出f:x₀ → x₀,这是多态类型吗?不是。因为我们并没有定义什么是“多态类型”。不妨采用System F的类型记法,对这样的函数进行“泛化”:

f:ψ(x)f:x.ψ(x)\frac{f:ψ(x₀)}{f:∀x₀.ψ(x₀)}

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

f:x.ψ(x)f:ψ(a)\frac{f:∀x.ψ(x)}{f:ψ(a)}

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

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

然而,我们之前的论述,都是在一种特殊λ表达式的基础上,语法上只有三个东西:

  1. 1,2,true,false,+之类的常量
  2. λx.e的lambda表达式
  3. (e e)的函数调用

这样带来的问题是,即使λ表达式可以是“多态类型”的,λ表达式的参数仍然没法是多态类型的:

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

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

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

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

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

也就是说:

  1. 在表达式let var = e₁ in e₂中,e₁的类型被泛化。泛化方法为:
    • 当前环境 ΓΓ 中的自由变量为 F(Γ)F(Γ)
    • ee₁ 的自由变量为 F(e)F(e₁)
    • 遍历每一个在 F(e)F(Γ)F(e₁) - F(Γ) 的自由变量 xxᵢe:te₁:t 变为 e:x.te₁:∀xᵢ.t
  2. 每当从当前环境 ΓΓ 中引用一个泛型变量 e:te:t₁ 时,用一个新的类型变量例化 e:te:t₁ 直到 tt₁ 不再含有

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

值限制

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

let s f g x = f x (g x)
let k x y = x
let i = s k k
let ϕ = s (k (s i)) k

你会发现,在Haskell中,这是没问题的:

1

但是在F#中,这会报错:

2

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

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

如果给出这样的程序:

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

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

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

ref  : 'a -> 'a ref
(!)  : 'a ref -> 'a
(:=) : 'a ref -> 'a -> unit

上面的程序写作:

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

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

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

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

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

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

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

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

²Simple imperative polymorphism, ANDREW K. WRIGHT

量词的位置?

在system F中,量词可以出现在一个类型的任意位置。比如x.(xy.y)∀x.(x → ∀y.y). 事实上,System F虽然无法构造y组合子(有悖于强规范性),但却可以编码类似于λ表达式中(xx)(x x)的结构:

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

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

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

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

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

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

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

λ(x:t).(x t)xλ(x:t₁).(x\ t₂)x

有没有一个算法,可以得到通过这个表达式得到tt₁tt₂的值呢?

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进一步告诉我们,如果不给出显式的tt₁tt₂,只要求检查最后的类型,那么这个问题还是不可判定的。

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

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