Опишите вывод типа Damas-Milner таким образом, чтобы ученик CS101 мог понять

Ответ 1

Дамас Милнер - это просто структурированное использование унификации.

Когда он повторяется в выражении лямбда, он составляет новое имя переменной. Когда вы в суб-термине найдете эту переменную, используемую таким образом, который потребует определенного типа, он записывает объединение этой переменной и этого типа. Если он когда-либо пытается объединить два типа, которые не имеют смысла, например, говоря, что отдельная переменная является как Int, так и функцией из a → b, то она кричит на вас за что-то плохое.

Кроме того, этот алгоритм часто называют типом. Это действительно система вывода? Я думал, что это только выводит типы.

Вывод типов - это вывод типа. Проверка, чтобы увидеть, что аннотации типа действительны для данного термина, является проверка типа. Это разные проблемы.

Если это так, это означает, что интересной частью является сама система типов, а не система вывода типов.

Обычно говорят, что системы типа стиля Хиндли-Милнера сбалансированы на пороге. Если вы добавите гораздо больше функциональности, становится невозможным вывести типы. Таким образом, системные расширения типа, которые вы можете сложить поверх системы типа типа Хиндли-Милнера, не разрушая его свойств вывода, действительно являются интересными частями современных функциональных языков. В некоторых случаях мы смешиваем вывод типа и проверку типов, например, в Haskell многие современные расширения не могут быть выведены, но их можно проверить, поэтому они требуют аннотации типов для расширенных функций, таких как полиморфная рекурсия.

Ответ 2

Википедия дает описание алгоритма, который, насколько я могу судить, составляет одно слово: "унификация". Это все? Если это так, это означает, что интересной частью является сама система типов, а не система вывода типов.

IIRC, интересная часть алгоритма вывода типа Дамаса-Мильнера W заключается в том, что он имеет наиболее общие типы.