f# - F# 中的 Hindley Milner 类型推断

Question

有人可以在以下 F# 程序中逐步解释类型推断：

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

我特别想逐步了解 Hindley Milner 的统一过程是如何运作的。

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

然后我们需要一个 for 类型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

我跳过了一些琐碎的步骤，但我认为您可以了解它的工作原理。