Правильная форма letrec в системе типа Hindley-Milner?

У меня возникли проблемы с пониманием определения letrec для системы HM, которое приведено в Википедии, здесь: https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions

Для меня правило грубо переводится по следующему алгоритму:

  • выводить типы на все в разделе определения letrec
    • присваивать переменные временного типа каждому определенному идентификатору
    • рекурсивно обрабатывать все определения с временными типами
    • в парах, унифицируйте результаты с исходными временными переменными
  • закрыть (с forall) выводимые типы, добавить их в базу (контекст) и вывести типы выражения с ней

У меня возникают проблемы с такой программой:

letrec
 p = (+)     --has type Uint -> Uint -> Uint
 x = (letrec
       test = p 5 5
     in test)
in x

Поведение, которое я наблюдаю, выглядит следующим образом:

  • определение p получает временный тип a
  • определение x также получает некоторый временный тип, но теперь из нашей области
  • in x, определение test получает временный тип t
  • p получает временный тип a из области действия, используя правило HM для переменной
  • (f 5) обрабатывается по правилу HM для приложения, итоговый тип - b (и унификация, которая (a объединяется с Uint -> b)
  • ((p 5) 5) обрабатывается по тому же правилу, что приводит к большему количеству унификаций и типу c, a теперь в результате объединяется с Uint -> Uint -> c
  • теперь тест закрывается, чтобы ввести forall c.c
  • переменная test in test получает экземпляр типа (или forall c.c) со свежими переменными, в соответствии с правилом HM для переменной, в результате чего test :: d (который унифицирован с test::t справа)
  • в результате x эффективно набирает d (или t, в зависимости от настроения унификации)

Проблема: x должен, очевидно, иметь тип Uint, но я не вижу, чтобы эти двое могли объединяться для создания типа. Существует потеря информации, когда тип test закрывается, и экземпляр снова появляется, что я не уверен, как преодолеть или подключиться к подстановкам/унификации.

Любая идея, как алгоритм должен быть исправлен для корректной печати x::Uint? Или это свойство системы HM и просто не будет вводить такой случай (что я сомневаюсь)?

Обратите внимание, что это было бы вполне нормально со стандартным let, но я не хотел обфускать пример с помощью рекурсивных определений, которые невозможно обработать с помощью let.

Заранее спасибо

Ответы

Ответ 1

Отвечая на мой собственный вопрос:

Определение в Wiki неверно, хотя оно работает в определенной степени, по крайней мере, для проверки типов.

Самый простой и правильный способ добавить рекурсию к системе HM - использовать предикат fix с определением fix f = f (fix f) и введите forall a. (a->a) -> a. Взаимная рекурсия обрабатывается двойной фиксированной точкой и т.д.

Подход Haskell к проблеме (описанный в https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b#binding-groups) (примерно), чтобы получить неполный тип для всех функций, а затем запустить еще раз, чтобы проверить их друг против друга.