я пытаюсь вывести тип следующего выражения:
let rec fix f = f (fix f)
, которому следует присвоить тип (a -> a) -> a
После использования восходящего алгоритма (описанного в , обобщающего алгоритмы вывода типа Хиндли-Милнера ) с добавленным ниже правилом:
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
. Надеюсь, это очевидно для кого-то.