Hindley Milner Tipo Inferenza in F#

Question

Qualcuno può spiegare l'inferenza del tipo passo dopo passo nel seguire il programma F#:

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

Voglio specificamente vedere Step by Step come funziona il processo di unificazione in Hindley Milner.

Answer 1

Cose divertenti!

Per prima cosa inventiamo un tipo generico per Sumlist:x -> y

E ottieni le equazioni semplici:t(lst) = x; t(match ...) = y

Ora aggiungi l'equazione:t(lst) = [a] per colpa di (match lst with [] ...)

Quindi l'equazione:b = t(0) = Int; y = b

Poiché 0 è un possibile risultato della partita:c = t(match lst with ...) = b

Dal secondo modello:t(lst) = [d]; t(hd) = e; t(tl) = f; f = [e]; t(lst) = t(tl); t(lst) = [t(hd)]

Indovina un tipo (un tipo generico) per hd: g = t(hd); e = g

Quindi abbiamo bisogno di un tipo per sumList, quindi per ora avremo solo un tipo di funzione insignificante:h -> i = t(sumList)

Quindi ora sappiamo:h = f; t(sumList tl) = i

Quindi dall'aggiunta otteniamo:Addable g; Addable i; g = i; t(hd + sumList tl) = g

Ora possiamo iniziare l'unificazione:

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

Ho saltato alcuni passaggi banali, ma penso che tu possa ottenere come funziona.