[html]2010, Роман Душкин, Модель типизации Хиндли — Милнера и пример её реализации на языке Haskell
<br />
&nbsp;&nbsp;&nbsp;&nbsp;<a href="http://www.fprog.ru/2010/issue5/roman-dushkin-hindley-milner/">http://www.fprog.ru/2010/issue5/roman-dushkin-hindley-milner/</a>[/html]

Для некоторого языка программирования можно определить (описать, сформулировать) два синтаксиса:
- полный синтаксис, с явным определением всех типов всех значений
- сокращённый синтаксис (в котором о типах значений можно догадаться из контекста, то есть использованных над значением функций и операций)
В процесс компиляции компилятор:
- отображает текст программы в сокращённом синтаксисе на термины алгоритма Хиндли-Милнера;
- выполняет алгоритм Хиндли-Милнера с целью вычисления типов значений;
- восстанавливает полный синтаксис, используя типы значений (это может происходить неявно);
- использует полученные знания о типах значений для следующих этапов компиляции (например для генерирования кода).

Всё это делается для того, чтобы программисту было меньше писа́ть текста, записывать программу в сокращённом синтаксисе, а не в полном.

---

Однако типы используются для других разных целей, например для укладки значений в стек при вызове подпрограммы,
для определения времени жизни значений в куче в Rust.
Поэтому про систему типов нужно говорить и отдельно от алгоритма Хиндли-Милнера и лямбда-исчислений,
точнее, в идеале было бы хорошо иметь
математическую модель реальных процессоров (построить связь между лямбда-исчислением и моделью вычислений, приближенной к процессору).
Кое-что в природе существует, но связи с лямбда-исчислением я пока не видел
(или видел, но не понял. Functional Specification, это ведь не обязательно относится к "функциональному программированию"?).

---

1920-е
  алгоритм унификации и типизации были предложены
  К. Мередитом (в 1950-х годах)
  Дж. Моррисом (1968 год)
  предположительно, А. Тарским (вообще в 1920-х годах).

1965, Дж. А. Робинзон,
   предложил "принцип резолюции"
1969 год, Роджер Хиндли
  доказал, что его алгоритм выводит наиболее общий тип выражения
1978 год, Робин Милнер
1982 год, Луис Дамас
   доказал, что алгоритм Милнера полон и позволяет выводить типы в полиморфных системах

Базовый вариант оперирует только теми сущностями, которые используются в простом типизированном λ-исчислении —  в результате работы алгоритма для λ-термов получаются только базовые типы из известного множества (хотя непосредственно в процессе вывода используются типовые переменные).

Алгоритм автоматического вывода типов строит систему уравнений, неизвестными в которой являются типы, после чего решает эту систему, находя неизвестные значения.

Для решения построенной системы уравнений применяется процедура унификации. Её суть заключается в сравнении типов и попытках сопоставить типы друг с другом.

унификация - процедура приведения к наиболее общему типу.

Наиболее общим типом называется такой тип заданного выражения, к которому можно привести любой другой тип, который может быть приписан этому выражению.

Тип может быть представлен в виде дерева,
в узлах которого находятся конструкторы типов, а в листьевых вершинах — базовые типы.

У нас это преобразования из целого в плавающее.

Правила вывода представляют собой продукции, записанные в форме дробей. «Числитель» дроби представляет собой посылку правила (антецедент), «знаменатель», соответственно, — заключение правила (консеквент). Если антецедент правила истиннен, то по этому правилу можно заключить, что истиннен и консеквент.

Отредактировано ВежливыйЛис (2021-12-22 05:58:44)