Вивід типів

Алгоритм Гіндлі – Мілнера — механізм виводу типів виразів, який реалізується в мовах програмування, які базуються на системі типів Гіндлі – Мілнера, таких як ML (перша мова цього сімейства), Standard ML, OCaml, Haskell, F#, Fortress та Boo. Мова Nemerle використовує цей алгоритм з рядом необхідних змін[2].

Механізм виведення типів базується на можливості автоматично повністю або частково виводити тип виразу, отриманого за допомогою обчислення деякого виразу. Оскільки цей процес систематично проводиться під час трансляції програми, транслятор часто може вивести тип змінної або функції без явного вказування типів цих об'єктів. В багатьох випадках можна опускати явні декларації типів — це можна робити для достатньо простих об'єктів, або для мов з простим синтаксисом. Наприклад, в мові Haskell реалізований достатньо потужний механізм виведення типів, тому явного вказування типів функцій в цій мові програмування не потрібно. Програміст може вказати тип функції явно для того, щоб обмежити її використання тільки для конкретних типів даних, або для більш структурованого оформлення початкового коду.

Для того, щоб отримати інформацію для коректного виведення типу виразу в умовах відсутності явної декларації типу цього виразу, транслятор або збирає таку інформацію з явних декларацій типів підвиразів (змінних, функцій), які входять до виразу, що вивчається, або використовує неявну інформацію про типи атомарних значень. Такий алгоритм не завжди допомагає визначити тип виразу, особливо у випадку використання функцій вищих порядків і параметричного поліморфізму достатньо складної природи. Тому в складних випадках, коли виникає необхідність уникнути неоднозначностей, рекомендується явно вказувати тип виразів.

Сама модель типізації базується на алгоритмі виведення типів виразів, який має як джерело механізм отримання типів виразів, що використовується в типізованому λ-численні, який був запропонований в 1958 році Г. Каррі і Р. Фейсом. Далі вже Роджер Гіндлі в 1969 році розширив сам алгоритм і довів, що він виводить найзагальніший тип виразу. В 1978 році Робін Мілнер незалежно від Р. Гіндлі довів властивості еквівалентного алгоритму. І, нарешті, в 1985 році Луіс Дамас остаточно показав, що алгоритм Мілнера є завершеним і може використовуватись для поліморфних типів. У зв'язку з цим алгоритм Гіндлі – Мілнера інколи називають також і алгоритмом Дамаса – Мілнера.

Система типів визначається в моделі Гіндлі – Мілнера наступним чином:

1. Примітивні типи ${\displaystyle v}$ є типами виразів.
2. Параметричні змінні типів α є типами виразів.
3. Якщо ${\displaystyle \sigma _{1}}$ і ${\displaystyle \sigma _{2}}$ — типи виразів, то тип ${\displaystyle \sigma _{1}\rightarrow \sigma _{2}}$ є типом виразів.
4. Символ ${\displaystyle \bot }$ є типом виразів.

Вирази, типи яких обчислюються, визначаються досить стандартним чином:

1. Константи є виразами.
2. Змінні є виразами.
3. Якщо ${\displaystyle e_{1}}$ і ${\displaystyle e_{2}}$ — вирази, то (${\displaystyle e_{1}e_{2}}$) — вираз.
4. Якщо ${\displaystyle v}$ — змінна, а ${\displaystyle e}$ — вираз, то ${\displaystyle \lambda v.e}$ — вираз.

Кажуть, що тип ${\displaystyle \sigma _{1}}$ є екземпляром типу ${\displaystyle \sigma _{2}}$, коли існує деяке перетворення ${\displaystyle \rho }$ таке, що:

${\displaystyle \sigma _{1}=\rho (\sigma _{2})}$

При цьому зазвичай вважається, що на перетворення типів ${\displaystyle \rho }$ накладаються обмеження, які полягають в тому, що:

1. ${\displaystyle \rho (\sigma _{1}\rightarrow \sigma _{2})=\rho (\sigma _{1})\rightarrow \rho (\sigma _{2})}$
2. ${\displaystyle \rho (v)=v}$

Сам алгоритм виведення типів складається з двох кроків — генерування системи рівнянь і наступне розв'язування цих рівнянь.

Побудова системи рівнянь базується на наступних правилах:

1. ${\displaystyle f\Gamma v=\tau }$ — в тому випадку, якщо зв'язування ${\displaystyle v:\tau }$ знаходиться в ${\displaystyle \Gamma }$.
2. ${\displaystyle f\Gamma (ef)=\tau }$ — в тому випадку, якщо ${\displaystyle \tau _{1}=\tau _{2}\rightarrow \tau }$, де ${\displaystyle \tau _{1}=f\Gamma e}$ і ${\displaystyle \tau _{2}=f\Gamma f}$.
3. ${\displaystyle f\Gamma (\lambda v.e)=\tau \rightarrow \tau _{e}}$ — в тому випадку, якщо ${\displaystyle \tau _{e}=f\Gamma 'e}$ і ${\displaystyle \Gamma '}$ є розширенням ${\displaystyle \Gamma }$ зв'язуванням ${\displaystyle v:\tau }$.

В цих правилах під символом ${\displaystyle \Gamma }$ розуміється набір зв'язувань змінних з їх типами (середовище типізації):

${\displaystyle \Gamma =v_{1}:A_{1},v_{2}:A_{2},\ldots ,v_{n}:A_{n}}$

Розв'язування побудованої системи рівнянь базується на алгоритмі уніфікації. Це достатньо простий алгоритм. Є деяка функція ${\displaystyle u}$, яка приймає на вхід рівняння типів і повертає деяку підстановку. Підстановка — це просто проекція змінних типів на самі типи. Такі підстановки можуть обчислюватись різними способами, які залежать від конкретної реалізації алгоритму Гіндлі – Мілнера.