haskell - 使用 Hindley Milner 和约束​​推断递归表达式

Question

我试图推断以下表达式的类型：

let rec fix f = f (fix f)

应该给出类型(a -> a) -> a

在使用自下而上算法（在泛化hindley-milner 类型推理算法中描述）并添加以下规则后：

           a1, c1 |-BU e1 : t1     B = fresh var
---------------------------------------------------------
a1\x, c1 U {t' == B | x : t' in A} |-BU let rec x = e1 : t

我剩下以下类型：t1 -> t2

以及以下约束：

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

我看不出这些约束是如何解决的，所以我只剩下 type 了(a -> a) -> a。我希望有人能清楚地看到我是否出错了。

完整的源代码在这里

Answer 1

不应该有一个t7for firstfix f吗？这些给出了约束：

t7 = t2
t0 = t1 -> t7

从中你应该能够推断出，t4 = t2然后t0 = (t2 -> t2) -> t2。