Вивід типів

Ви́від ти́пів (англ. type inference) — в програмуванні можливість компілятора самому логічно вивести тип значення у виразу. Вперше механізм виведення типів був представлений в мові ML, де компілятор завжди виводить найзагальніший поліморфний тип для будь-якого виразу. Це не тільки скорочує розмір початкового коду і підвищує його лаконічність, але і часто підвищує повторне використання коду^[1].

Вивід типів є характерним для функціональних мов програмування, хоча з часом ця можливість частково з'явилася і в об'єктно-орієнтованих мовах програмування (C#, D, Visual Basic .NET, C++11, Vala, Go), де вона обмежується можливістю опустити тип ідентифікатора у визначенні з ініціалізацією (див. синтаксичний цукор). Наприклад:

var s = "Hello, world!";  // Тип змінної s (string) виведений з ініціалізатора

Алгоритми

Алгоритм Гіндлі – Мілнера

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

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

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

Сама модель типізації базується на алгоритмі виведення типів виразів, який має як джерело механізм отримання типів виразів, що використовується в типізованому λ-численні, який був запропонований в 1958 році Г. Каррі і Р. Фейсом. Далі вже Роджер Гіндлі^[en] в 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}$, яка приймає на вхід рівняння типів і повертає деяку підстановку. Підстановка — це просто проєкція змінних типів на самі типи. Такі підстановки можуть обчислюватись різними способами, які залежать від конкретної реалізації алгоритму Гіндлі – Мілнера.

Див. також

• Качина типізація
• Приведення типів

Примітки

1. Andrew W. Appel. A Critique of Standard ML // Princeton University, revised version of CS-TR-364-92. — 1992.(англ.)
2. Michał Moskal. Type Inference with Deferral // Institute of Computer Science, University of Wrocław. — 2005. Архівовано з джерела 4 березня 2016. Процитовано 29 липня 2015.(англ.)

Посилання

• Реалізація алгоритму Гіндлі-Мілнера на Perl (англ.)
• Archived e-mail message [Архівовано 6 лютого 2021 у Wayback Machine.] by Roger Hindley, explains history of type inference (англ.)
• Polymorphic Type Inference [Архівовано 10 квітня 2011 у Wayback Machine.] by Michael Schwartzbach, gives an overview of Polymorphic type inference. (англ.)
• Principal type-schemes for functional programs. A re-typeset copy of the Damas and Milner paper which described the soundness and completeness proofs. (англ.)
• Tutorial and complete implementation in Standard ML The tutorial includes some of the logical history of type systems as well as a detailed description of the algorithm as implemented. Some typographic errors in the original Damas Milner paper are corrected. (англ.)
• Basic Typechecking [Архівовано 11 серпня 2015 у Wayback Machine.] paper by Luca Cardelli, describes algorithm, includes implementation in Modula-2 (англ.)
• Implementation [Архівовано 15 лютого 2015 у Wayback Machine.] of Hindley-Milner type inference in Scala, by Andrew Forrest (retrieved July 30, 2009) (англ.)
• Implementation of Hindley-Milner in Perl 5, by Nikita Borisov на сайті Wayback Machine (архівовано лютий 18, 2007). (англ.)
• What is Hindley-Milner? (and why is it cool?) [Архівовано 10 серпня 2015 у Wayback Machine.] Explains Hindley-Milner, examples in Scala (англ.)
• http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ [Архівовано 30 грудня 2014 у Wayback Machine.] Модель типізації Гіндлі-Мілнера і приклад її реалізації на мові Haskell (рос.)