7
Estoy tratando de inferir el tipo de la siguiente expresión:Deducir expresiones recursivas utilizando Hindley Milner y limitaciones
let rec fix f = f (fix f)
que debe darse el tipo (a -> a) -> a
Después de usar abajo hacia arriba algoritmo (descrito en generalizadoras algoritmos de tipo hindley-Milner inferencia) con la regla añadida a continuación:
a1, c1 |-BU e1 : t1 B = fresh var
---------------------------------------------------------
a1\x, c1 U {t' == B | x : t' in A} |-BU let rec x = e1 : t
me quedo con el tipo siguiente: t1 -> t2
y las siguientes limitaciones:
t0 = fix
t1 = f
t2 = f (fix f)
t3 = f
t4 = fix f
t5 = fix
t6 = f
t3 = t1
t3 = t4 -> t2
t5 = t0
t5 = t6 -> t4
t6 = t1
no puedo ver cómo estas limitaciones pueden ser resueltos de manera que me quedo con el tipo (a -> a) -> a. Espero que sea obvio para alguien ver si me estoy equivocando.
Tenga en cuenta que 'let rec' debe ser simplemente' let'; de lo contrario, solo está definiendo una función 'rec :: ((a -> b) -> a) -> (a -> b) -> b'. –
@ Ptharien'sFlame Lo sentimos, el ejemplo del código wasnt en haskell pero un lenguaje de estilo ML. –
De acuerdo, es solo que tenía la pregunta etiquetada con "haskell", así que supuse que ese era el idioma con el que estaba trabajando. ¡Lo siento! –