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