我正在尝试推断以下表达式的类型:
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
。希望有人能看出我的错误所在。完整的源代码请点击 这里。
let rec
应该简单地写成let
,否则你只是在定义一个函数rec :: ((a -> b) -> a) -> (a -> b) -> b
。 - Ptharien's Flame