Hindley Milner Type Inference in F #

Question

Qualcuno può spiegare passo passo tipo di inferenza nel seguente programma F #:

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

In particolare mi voglio vedere passo passo come funziona il processo di unificazione in Hindley Milner.

Answer 1

Cose divertenti!

prima cosa inventare un tipo generico per listaSomma: x -> y

e ottenere i semplici equazioni: t(lst) = x; t(match ...) = y

Ora si aggiunge l'equazione: t(lst) = [a] a causa 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)]

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

Poi abbiamo bisogno di un tipo per sumList, quindi ci limiteremo a ottenere un tipo di funzione senza senso per ora: h -> i = t(sumList)

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

Poi l'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.