Я пытаюсь научить себя выводу типа Хиндли-Милнера, реализуя алгоритм W на языке, который я обычно использую, Clojure. У меня возникла проблема с выводом let, и я не уверен, что делаю что-то не так, или результат, который я ожидаю, требует чего-то вне алгоритма.
В основном, используя нотацию Haskell, если я попытаюсь вывести тип этого:
\a -> let b = a in b + 1
Я получаю это:
Num a => t -> a
Но я должен получить это:
Num a => a -> a
Опять же, я на самом деле делаю это в Clojure, но я не верю, что проблема специфична для Clojure, поэтому я использую нотацию Haskell, чтобы сделать ее более понятной. Когда я пробую это в Haskell, я получаю ожидаемый результат.
В любом случае, я могу решить эту конкретную проблему, преобразовав каждый let в приложение-функцию, например:
\a -> (\b -> b + 1) a
Но тогда я теряю let полиморфизм. Поскольку у меня нет никаких предварительных знаний о HM, мой вопрос заключается в том, что я что-то здесь упускаю, или это просто способ работы алгоритма.
ИЗМЕНИТЬ
На случай, если у кого-то возникнет аналогичная проблема и интересно, как я ее решил, я следил за Пошаговый алгоритм W. Внизу страницы 2 написано: «Иногда будет полезно расширить методы Types до списков». Поскольку это не казалось мне обязательным, я решил пропустить эту часть и вернуться к ней позже.
Затем я перевел функцию ftv для TypeEnv непосредственно в Clojure следующим образом: (ftv (vals env)). Поскольку я реализовал ftv как форму cond и не имел условия для seqs, он просто возвращал nil вместо (vals env). Это, конечно, именно та ошибка, которую система статического типа предназначена для отлова! Во всяком случае, я только что переопределил пункт в ftv, относящийся к карте env, на (reduce set/union #{} (map ftv (vals env))), и это работает.
