Модель типизации Хиндли - Милнера и пример её реализации на языке Haskell

[_adept_]

Модель типизации Хиндли - Милнера и пример её реализации на языке Haskell
Роман Душкин

Аннотация

Статья описывает алгоритм Хиндли - Милнера, используемый для автоматического

Comments

Курсы разгромного рецензирования

[nponeccop]

Я по-прежнему не понимаю, как рецензенты могли пропустить следующие чудовищные фразы. И это только в аннотации и на первых двух страницах. Неужели никто не увидел полной недопустимости этих фраз в журналах, претендующих на рациональность

Re: Курсы разгромного рецензирования

[nponeccop]

А объяснить ошибочность каждой фразы не можете?

Re: Курсы разгромного рецензирования

[nponeccop]

Могу, конечно, и в своих рецензиях объясняю, вплоть до приведения ссылок при сопротивлении рецензируемого автора. Но мне интересно найти рецензента, способного отыскать гадости хотя бы в половине этих фраз. Гадости, связанные со словоупортеблением, искажением исторической правды или просто неверными сведениями.

Скажем, фраза 13 представляет алгоритм W вариантом некоторого другого алгоритма. Какого? Во-первых, алгоритмы вывода типов для системы Хиндли-Милнера, для которого алгоритм W является частным случаем, существуют, но в статье не упоминаются вообще. Во-вторых, эти алгоритмы (например, алгоритм InferType, описанный в статье "Generalizing Hindley-Milner Type Inference
Algorithms" и алгоритм G, описанный в статье "Proofs of a Set of Hybrid Let-Polymorphic Type Inference Algorithms") не имеют ни к Хиндли, ни к Милнеру, никакого отношения и не названы их именами.

Re: Курсы разгромного рецензирования

[antilamer]

+1 к предыдущему оратору; часть приведенного звучит коряво и витиевато, но прямо-таки чудовищного ничего не вижу (статью пока не читал).

[beroal]

А вы уверены, что это «алгоритм W»? В «Luis Damas and Robin Milner. Principal type-schemes for functional programs.» ветка для аппликации выглядит проще, она не имеет вложенного case of.

[nponeccop]

С алгоритмом там интересный ляп. В разделе 6.2 описывается не алгоритм W, а более поздний алгоритм, с разделением на фазу построения и фазу решения уравнений. Алгоритм W, как видно из статьи Дамаса и Милнера, ничего не строит, а сразу выдает решение.

В разделе 4 описывается снова не алгоритм W, а более ранний алгоритм для STLC. Вдобавок, подстановки, одна из ключевых черт алгоритма W, вообще не генерируются, в результате все эти громоздкости с вложенными case of.

Ещё не забывайте, что у Милнера unify при отказе тупо бросает error, а Роман делает аккуратный монадический отказ.

А в статье Дамаса и Милнера алгоритм описан с опечатками - как раз в ветке аппликации перепутаны индексы - нету е1 и тау1.

[beroal]

offtopic: А зачем вы цеплялись к стилю, если в статье есть более серьёзные ошибки?

[nponeccop]

1) Я вообще не приводил никакого анализа - просто прочитал первые две страницы и выписал нехорошие фрагменты. Все подряд. Это не рецензия - это указание рецензентам, на что стоит обращать внимание.

2) Строго говоря, это не "витиеватость", не "стилистические ошибки", а подмена близких, но различных понятий. Стилилистика - это, скажем, излишнее использование канцелярита или вводных слов.

[beroal]

Кроме того, в программе ошибка.

> \x.\y.x ((\a.y) x)
ERROR: Can't unify type (g -> c) with (e).

*TypeInference> :t \x -> \y -> x ((\a -> y) x)
\x -> \y -> x ((\a -> y) x) :: (t -> t1) -> t -> t1

[beroal]

Ну знаете. Не настолько уж алгоритм W сложный. И мой вариант почему-то работает. И о необходимости β-редукции я слышу в первый раз - от Вас.

[beroal]

Ещё я надеялся, что будет хотя бы намёк, почему этот алгоритм является корректным. Ну да ладно, статья и так длиннючая.