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

Question

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

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

1. типов Infer на все в Частей letrec определения
   1. присвоить переменные временные типа для каждого определенного идентификатора
   2. рекурсивно обрабатывать все определения типов с временными
   3. в парах, объединить результаты с первоначальными временных переменных
2. близко (с forall) выведенный типы, добавить их к базису (контекст) и вывод типов выражения части с ним

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

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

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

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

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

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

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

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

Answer 1

Ответ на свой вопрос:

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

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

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