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.
fonte
2011-12-06 07:57:10
Penso che questo potrebbe appartenere ad un altro sito SE, ma non sono sicuro quale :) –
Se è possibile mi puoi dare un link a questo? Sarebbe utile. – riship89
Beh, penso che appartenga a Theo CS, ma non credo che lo accetterebbero.A meno che non venga un moderatore intelligente, immagino che rimarrà qui :) –