辛德雷米尔纳类型推断F＃

Question

有人可以解释一步一步的类型推断在下面的F＃程序：

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

我特别想一步看一步辛德雷米尔纳统一的过程中是如何工作的。

Answer 1

有趣的东西！

首先，我们发明了一种通用型的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)]

猜一种类型（通用型）hd： g = 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

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