Вывод типа Хиндли Милнера в 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

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