Hindley Milner类型推理在F#

有人可以在下面的F#程序中解释一步一步的类型推断:

let rec sumList lst =
    match lst with
    | [] -> 0
    | hd :: tl -> hd + sumList tl

我特别希望一步一步看到Hindley Milner的统一过程如何运作。


好玩的东西!

首先我们为sumList创建一个泛型类型: x -> y

并得到简单的方程: t(lst) = x ; t(match ...) = y

现在你添加方程: t(lst) = [a]因为(match lst with [] ...)

然后等式: b = t(0) = Int ; y = b

由于0是匹配的可能结果: c = t(match lst with ...) = b

从第二种模式: t(lst) = [d] ; t(hd) = e ; t(tl) = f ; f = [e] ; t(lst) = t(tl) ; t(lst) = [t(hd)]

猜测一个类型(一个泛型)为hdg = t(hd) ; e = g

然后我们需要一个sumList类型,所以我们现在只需要一个无意义的函数类型: h -> i = t(sumList)

所以现在我们知道: h = f ; t(sumList tl) = i

然后从添加我们得到: Addable g ; Addable i ; g = i ; t(hd + sumList tl) = g

现在我们可以开始统一:

t(lst) = t(tl) => [a] = f = [e] => a = e

t(lst) = x = [a] = f = [e] ; h = t(tl) = x

t(hd) = g = i / i = y => y = t(hd)

x = t(lst) = [t(hd)] / t(hd) = y => x = [y]

y = b = Int / x = [y] => x = [Int] => t(sumList) = [Int] -> Int

我跳过了一些微不足道的步骤,但我认为你可以得到它的工作原理。

链接地址: http://www.djcxy.com/p/80883.html

上一篇: Hindley Milner Type Inference in F#

下一篇: Milner algorithm in Java