Damas Milner - это просто структурированное использование объединения.
Когда оно повторяется в лямбда-выражении, оно создает новое имя переменной. Когда вы, в подслове, находите эту переменную, используемую таким образом, который требует заданного типа, она записывает объединение этой переменной и этого типа. Если он когда-нибудь попытается объединить два типа, которые не имеют смысла, как, например, сказать, что отдельная переменная является одновременно Int и функцией из a -> b, то он кричит на вас за то, что вы сделали что-то плохое.
Кроме того, часто говорят, что этот алгоритм делает вывод типа. Это действительно система логического вывода? Я думал, что это только вывод типов.
Вывод типов является выводом типа. Проверка того, что аннотации типов действительны для данного термина, является проверкой типов. Это разные проблемы.
Если это так, это означает, что интересной частью является сама система типов, а не система вывода типов.
Обычно говорят, что системы типов в стиле Хиндли-Милнера сбалансированы на вершине. Если вы добавите гораздо больше функциональности, станет невозможно определить типы. Таким образом, расширения системы типов, которые вы можете наложить поверх системы типов стилей Хиндли-Милнера, не разрушая ее свойства вывода, действительно являются интересными частями современных функциональных языков. В некоторых случаях мы смешиваем вывод типов и проверку типов, например, в Haskell многие современные расширения не могут быть выведены, но могут быть проверены, поэтому они требуют аннотаций типов для расширенных функций, таких как полиморфная рекурсия.