Я смотрю на взаимосвязь между типизированным λ-исчислением и системой типов Хиндли-Милнера состоит в том, что типизированное λ-исчисление равно λ-калькул с добавлением типов.Вы можете сделать набранное λ-исчисление без необходимости система типов Хиндли-Милнера , например, все типы объявлены, они не выводятся.
Теперь, если вы былинаписать строго статически типизированный язык программирования на основе типизированного λ-исчисления и хотел опустить аннотации типов , позволяющие типам быть выведенными затем используется вывод типа , и, скорее всего, вы будете использовать систему типов Хиндли-Милнера или ее вариант.
Еще один способ подумать об этом - при созданииЯзык программирования, основанный на набранном λ-исчислении , состоит в том, что компилятор будет иметь фазы , один из которых будет использовать систему типов Хиндли-Милнера .Порядок фаз будет следующим:
- Проверка синтаксиса - Lexer
- Семантическая проверка - Parser
- Вывод типа - Система типов Хиндли-Милнера
- Проверка типа
- ...
Еще один способ думать об этом состоит в том, что система имеет набор правил типа и что система типов Хиндли-Милнера является системой конкретного типа сопределенный набор правил типа.Одним из основных преимуществ системы типов Хиндли-Милнера является то, что она экономит время для выведения типов, а также имеет множество правил набора искомых в функциональном программировании Например, Let-полиморфизм и параметрический полиморфизм .В реальном мире, если вы создаете язык программирования и хотите, чтобы типы выводились, вы хотите, чтобы это было сделано за разумное количество времени, например, за секунды.Так как вывод может привести к комбинаторному взрыву , часто ищут эффективный набор правил, и это является одной из главных причин, почему система типа Хиндли-Милнера так частоиспользуется или на него ссылаются.
Для реальных языков программирования, основанных на набранном λ-исчислении см. Система F .