[Перевод] Итак, вы всё ещё не понимаете Хиндли-Милнера? Часть 1
Как-то мы сидели в баре с Джошем Лонгом и ещё несколькими друзьями с работы, когда он обнаружил, что я на «эй, ты!» с математикой. А он как раз недавно наткнулся на вот этот вопрос на StackOverflow и сейчас спросил меня, что это означает: 
Однако, перед выяснением смысла данной китайской грамоты, думаю, стоит в принципе получить представление о том, для чего вообще это нужно. Пост в блоге Даниэля Спивака (перевод) даёт по-настоящему хорошее объяснение конечной цели алгоритма Хиндли-Милнера (в дополнение к углубленному примеру его применения): Функционально говоря, Хиндли-Милнер (или Дамас-Милнер) — это алгоритм для вывода типов, основанный на рассмотрении того, как они используются. Он буквально формализует интуитивное знание о том, что тип может быть выведен через функционал, который он поддерживает.
Итак, мы хотим формализовать алгоритм вывода типа для любого заданного выражения. В этом посте я собираюсь остановиться на том, что означает «формализовать что-то», а затем описать «кирпичики» формализации Хиндли-Милнера. Во второй части я дам более конкретное описание этих блоков. Наконец, в третьей части я переведу вопрос со StackOverflow.Читать дальше →
