Вывод типа 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)]

Угадайте тип (общий тип) для 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

Я пропустил некоторые тривиальные шаги, но я думаю, вы можете понять, как это работает.