Просмотр кода страницы Вывод типов

{{Типизация данных}}
'''Вывод типов''' ({{lang-en|type inference}}) — в [[Программирование|программировании]] возможность [[компилятор]]а самому логически вывести [[Тип данных|тип значения]] у [[Выражение (информатика)|выражения]]. Впервые [[Машина вывода|механизм вывода]] типов был представлен в языке [[ML]], где компилятор всегда выводит наиболее общий [[Параметрический полиморфизм|полиморфный]] тип для всякого выражения. Это не только сокращает размер исходного кода и повышает его лаконичность, но и нередко повышает [[повторное использование кода]]<ref>{{статья
|заглавие = A Critique of Standard ML
|автор = Andrew W. Appel
|издательство = Princeton University, revised version of CS-TR-364-92
|год = 1992
|ссылка =
|ref = Appel - A Critique of Standard ML
}}</ref>.

Вывод типов характерен для [[Язык функционального программирования|функциональных языков программирования]], хотя со временем он был частично реализован и в [[Объектно-ориентированный язык программирования|объектно-ориентированных языках]] ([[C Sharp|C#]], [[D (язык программирования)|D]], [[Visual Basic .NET]], [[Nim]], [[C++11]], [[Vala]], [[Java]]{{efn|поддержка добавлена в [[Java#Java SE 10|Java SE 10]]}}), где ограничивается возможностью опустить тип идентификатора в определении с инициализацией (см. [[синтаксический сахар]]). Например:
<source lang="javascript">
var s = "Hello, world!";  // Тип переменной s (от string) выведен исходя из инициализатора
</source>

== Алгоритмы ==

=== Алгоритм Хиндли — Милнера ===
{{falseredirect|Система типов Хиндли — Милнера}}
Алгоритм Хи́ндли — Ми́лнера — механизм вывода типов выражений, реализуемый в языках программирования, основанных на [[Система типов Хиндли — Милнера|системе типов Хиндли — Милнера]], таких как [[ML]] (первый язык этого семейства), [[Standard ML]], [[OCaml]], [[Haskell]], [[F Sharp|F#]], [[Fortress]] и [[Boo]]. Язык [[Nemerle]] использует этот алгоритм с рядом необходимых изменений<ref>{{статья
|автор = Michał Moskal
|заглавие = Type Inference with Deferral
|publisher = Institute of Computer Science, University of Wrocław
|год = 2005
|ссылка = http://research.microsoft.com/en-us/um/people/moskal/pdf/msc.pdf
|archive-date = 2016-03-04
|archive-url = https://web.archive.org/web/20160304085538/http://research.microsoft.com/en-us/um/people/moskal/pdf/msc.pdf
}}</ref>.

Механизм вывода типов основан на возможности автоматически полностью или частично выводить тип выражения, полученного при помощи вычисления некоторого выражения. Так как этот процесс систематически производится во время трансляции программы, транслятор часто может вывести тип переменной или функции без явного указания типов этих объектов. Во многих случаях можно опускать явные декларации типов — это можно делать для достаточно простых объектов, либо для языков с простым синтаксисом. Например, в языке [[Haskell]] реализован достаточно мощный механизм вывода типов, поэтому указание типов функций в этом языке программирования не требуется. Программист может указать тип функции явно для того, чтобы ограничить её использование только для конкретных типов данных, либо для более структурированного оформления исходного кода.

Для того, чтобы получить информацию для корректного вывода типа выражения в условиях отсутствия явной декларации типа этого выражения, транслятор либо собирает такую информацию из явных деклараций типов подвыражений (переменных, функций), входящих в изучаемое выражение, либо использует неявную информацию о типах атомарных значений. Такой алгоритм не всегда помогает определить тип выражения, особенно в случаях использования [[Функция высшего порядка|функций высших порядков]] и [[Параметрический полиморфизм|параметрического полиморфизма]] достаточно сложной природы. Поэтому в сложных случаях, когда есть необходимость избежать неоднозначностей, рекомендуется явно указывать тип выражений.

Сама модель типизации основана на алгоритме вывода типов выражений, который имеет своим источником механизм получения типов выражений, используемый в типизированном [[Лямбда-исчисление|λ-исчислении]], который был предложен в [[1958]] г. [[Карри, Хаскелл|Х. Карри]] и Р. Фейсом. Далее уже́ [[Хиндли, Рождер|Роджер Хиндли]] в [[1969]] г. расширил сам алгоритм и доказал, что он выводит наиболее общий тип выражения. В [[1978]] г. [[Милнер, Робин|Робин Милнер]] независимо от Р. Хиндли доказал свойства эквивалентного алгоритма. И, наконец, в [[1985]] г. [[Дамас, Луис|Луис Дамас]] окончательно показал, что алгоритм Милнера является законченным и может использоваться для полиморфных типов. В связи с этим алгоритм Хиндли — Милнера иногда называют также и '''''алгоритмом Дамаса — Милнера'''''.

Система типов определяется в модели Хиндли — Милнера следующим образом:

# Примитивные типы <math>\tau</math> являются типами выражений.
# Параметрические переменные типов α являются типами выражений.
# Если <math>\sigma_{1}</math> и <math>\sigma_{2}</math> — типы выражений, то тип <math>\sigma_{1} \rightarrow \sigma_{2}</math> является типом выражений.
# Символ <math>\bot</math> является типом выражений.

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

# Константы являются выражениями.
# Переменные являются выражениями.
# Если <math>e_{1}</math> и <math>e_{2}</math> — выражения, то (<math>e_{1} e_{2}</math>) — выражение.
# Если <math>v</math> — переменная, а <math>e</math> — выражение, то <math>\lambda v.e</math> — выражение.

Говорят, что тип <math>\sigma_{1}</math> является экземпляром типа <math>\sigma_{2}</math>, когда имеется некое преобразование <math>\rho</math> такое, что:

<math>\sigma_{1} = \rho(\sigma_{2})</math>

При этом обычно полагается, что на преобразования типов <math>\rho</math> накладываются ограничения, заключающиеся в том, что:

# <math>\rho(\sigma_{1} \rightarrow \sigma_{2}) = \rho(\sigma_{1}) \rightarrow \rho(\sigma_{2})</math>
# <math>\rho(\tau) = \tau</math>

Сам алгоритм вывода типов состоит из двух шагов — генерация системы уравнений и последующее решение этих уравнений.

==== Построение системы уравнений ====
Построение системы уравнений основано на следующих правилах:

# <math>\Gamma v = \tau</math> — в том случае, если связывание <math>v : \tau</math> находится в <math>\Gamma</math>.
# <math>\Gamma (g e) = \tau</math> — в том случае, если <math>\tau_{1} = \tau_{2} \rightarrow \tau</math>, где <math>\tau_{1} = \Gamma g</math> и <math>\tau_{2} = \Gamma e</math>.
# <math>\Gamma (\lambda v.e) = \tau \rightarrow \tau_{e}</math> — в том случае, если <math>\tau_{e} = \Gamma' e</math>, где  <math>\Gamma'</math> это <math>\Gamma</math> с добавленным связыванием <math>v : \tau</math>.

В этих правилах под символом <math>\Gamma</math> понимается набор связываний переменных с их типами:

<math>\Gamma = v_{1} : A_{1}, v_{2} : A_{2}, \ldots, v_{n} : A_{n}</math>

==== Решение системы уравнений ====
Решение построенной системы уравнений основано на [[алгоритм унификации|алгоритме унификации]]. Это достаточно простой алгоритм. Имеется некоторая функция <math>u</math>, которая принимает на вход уравнение типов и возвращает подстановку, которая делает левую и правую части уравнения одинаковыми («унифицирует» их). Подстановка — это просто проекция переменных типов на сами типы. Такие подстановки могут вычисляться различными способами, которые зависят от конкретной реализации алгоритма Хиндли — Милнера.

== См. также ==
* [[Утиная типизация]]
* [[Приведение типа]]

== Примечания ==

=== Комментарии ===
{{комментарии}}

=== Источники ===
{{примечания}}


== Ссылки ==
* [https://web.archive.org/web/20050911123640/http://www.cs.berkeley.edu/~nikitab/courses/cs263/hm.html Реализация алгоритма Хиндли-Милнера] на [[Perl]]{{ref|en}}
* [http://www.cis.upenn.edu/~bcpierce/types/archives/1988/msg00042.html Archived e-mail message] by Roger Hindley, explains history of type inference
* [https://web.archive.org/web/20110410102617/http://www.brics.dk/~mis/typeinf.pdf Polymorphic Type Inference] by Michael Schwartzbach, gives an overview of Polymorphic type inference.
* [https://web.archive.org/web/20120324053855/http://ian-grant.net/hm/milner-damas.pdf Principal type-schemes for functional programs.] A re-typeset copy of the Damas and Milner paper which described the soundness and completeness proofs.
* [https://web.archive.org/web/20120324053910/http://www.ian-grant.net/hm/ 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.
* [http://lucacardelli.name/Papers/BasicTypechecking.pdf Basic Typechecking] paper by Luca Cardelli, describes algorithm, includes implementation in [[Modula-2]]
* [https://dysphoria.net/2009/06/28/hindley-milner-type-inference-in-scala/ Implementation] of Hindley-Milner type inference in [[Scala (язык программирования)|Scala]], by Andrew Forrest (retrieved July 30, 2009)
* {{Cite web |url=http://www.cs.berkeley.edu/~nikitab/courses/cs263/hm.html |title=Implementation of Hindley-Milner in Perl 5, by Nikita Borisov |access-date=2009-03-12 |archive-url=https://web.archive.org/web/20070218103011/http://www.cs.berkeley.edu/~nikitab/courses/cs263/hm.html |archive-date=2007-02-18 |url-status=dead }}
* [https://web.archive.org/web/20150810222004/http://www.codecommit.com/blog/scala/what-is-hindley-milner-and-why-is-it-cool What is Hindley-Milner? (and why is it cool?)] Explains Hindley-Milner, examples in Scala
* http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ Модель типизации Хиндли-Милнера и пример её реализации на языке Haskell

{{нет сносок|дата=2013-11-26}}

[[Категория:Типы данных]]