Inferencia tipo Hindley Milner en f#
-
28-10-2019 - |
Pregunta
¿Alguien puede explicar la inferencia de tipo paso a paso en el siguiente programa F#:
let rec sumList lst =
match lst with
| [] -> 0
| hd :: tl -> hd + sumList tl
Específicamente quiero ver paso a paso cómo funciona el proceso de unificación en Hindley Milner.
Solución
¡Cosas divertidas!
Primero inventamos un tipo genérico para Sumlist:x -> y
Y obtenga las ecuaciones simples:t(lst) = x
;
t(match ...) = y
Ahora agregas la ecuación:t(lst) = [a]
porque (match lst with [] ...)
Entonces la ecuación:b = t(0) = Int
; y = b
Dado que 0 es un posible resultado del partido:c = t(match lst with ...) = b
Del segundo patrón:t(lst) = [d]
;
t(hd) = e
;
t(tl) = f
;
f = [e]
;
t(lst) = t(tl)
;
t(lst) = [t(hd)]
Adivina un tipo (un tipo genérico) para hd
:
g = t(hd)
; e = g
Entonces necesitamos un tipo para sumList
, así que obtendremos un tipo de función sin sentido por ahora:h -> i = t(sumList)
Entonces ahora sabemos:h = f
;
t(sumList tl) = i
Luego, a partir de la adición, obtenemos:Addable g
;
Addable i
;
g = i
;
t(hd + sumList tl) = g
Ahora podemos comenzar la unificación:
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
Me salté algunos pasos triviales, pero creo que puedes obtener cómo funciona.