Inferring recursive expressions using Hindley Milner & constraints
functional-programming, haskell, hindley-milner, ml, type-inference
Solution
Shouldn't there be a `t7` for the first `fix f`? These give the constraints:
t7 = t2
t0 = t1 -> t7
From that you should be able to deduce that `t4 = t2` and then `t0 = (t2 -> t2) -> t2`.
Problem
I am trying to infer the type of the following expression: ``` let rec fix f = f (fix f) ``` which should be given the type `(a -> a) -> a` After using the bottom up algorithm (described in generalizing hindley-milner type inference algorithms) with the added rule below: ``` a1, c1 |-BU e1 : t1 B = fresh var --------------------------------------------------------- a1\x, c1 U {t' == B | x : t' in A} |-BU let rec x = e1 : t ``` i am left with the following type: `t1 -> t2` and the following constraints: ``` 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 ``` I cant see how these constraints can be solved such that i am left with the type `(a -> a) -> a`. I hope it is obvious for someone to see were i am going wrong. full source code here