使用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

我看不出如何解决这些限制，以至于我只剩下类型为 (a -> a) -> a。希望有人能看出我的错误所在。

完整的源代码请点击 这里。

- user181351

---

请注意，let rec 应该简单地写成 let，否则你只是在定义一个函数 rec :: ((a -> b) -> a) -> (a -> b) -> b。 - Ptharien's Flame

@Ptharien'sFlame 抱歉，代码示例不是使用Haskell编写的，而是使用ML风格的语言。 - user181351

好的，只是你把问题标记为“haskell”，所以我假设那是你正在使用的编程语言。抱歉！ - Ptharien's Flame

Answer 1

第一个fix f不应该有一个t7吗？以下是这些约束条件：

t7 = t2
t0 = t1 -> t7

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

- Sjoerd Visscher

---

你说得对，我在上面的规则中没有限制B为t！ - user181351