Вывод типов
Типизация данных |
|---|
Типобезопасность |
Вывод типов (англ. type inference) — в программировании возможность компилятора самому логически вывести тип значения у выражения. Впервые механизм вывода типов был представлен в языке ML, где компилятор всегда выводит наиболее общий полиморфный тип для всякого выражения. Это не только сокращает размер исходного кода и повышает его лаконичность, но и нередко повышает повторное использование кода[1].
Вывод типов характерен для функциональных языков программирования, хотя со временем он был частично реализован и в объектно-ориентированных языках (C#, D, Visual Basic .NET, C++11, Vala, Go, Java[a]), где ограничивается возможностью опустить тип идентификатора в определении с инициализацией (см. синтаксический сахар). Например:
var s = "Hello, world!"; // Тип переменной s (от string) выведен из инициализатора
Содержание
1 Алгоритмы
1.1 Алгоритм Хиндли — Милнера
1.1.1 Построение системы уравнений
1.1.2 Решение системы уравнений
2 См. также
3 Примечания
3.1 Комментарии
3.2 Источники
4 Ссылки
Алгоритмы |
Алгоритм Хиндли — Милнера |
Алгоритм Хи́ндли — Ми́лнера — механизм вывода типов выражений, реализуемый в языках программирования, основанных на системе типов Хиндли — Милнера (англ.), таких как ML (первый язык этого семейства), Standard ML, OCaml, Haskell, F#, Fortress и Boo. Язык Nemerle использует этот алгоритм с рядом необходимых изменений[2].
Механизм вывода типов основан на возможности автоматически полностью или частично выводить тип выражения, полученного при помощи вычисления некоторого выражения. Так как этот процесс систематически производится во время трансляции программы, транслятор часто может вывести тип переменной или функции без явного указания типов этих объектов. Во многих случаях можно опускать явные декларации типов — это можно делать для достаточно простых объектов, либо для языков с простым синтаксисом. Например, в языке Haskell реализован достаточно мощный механизм вывода типов, поэтому указание типов функций в этом языке программирования не требуется. Программист может указать тип функции явно для того, чтобы ограничить её использование только для конкретных типов данных, либо для более структурированного оформления исходного кода.
Для того, чтобы получить информацию для корректного вывода типа выражения в условиях отсутствия явной декларации типа этого выражения, транслятор либо собирает такую информацию из явных деклараций типов подвыражений (переменных, функций), входящих в изучаемое выражение, либо использует неявную информацию о типах атомарных значений. Такой алгоритм не всегда помогает определить тип выражения, особенно в случаях использования функций высших порядков и параметрического полиморфизма достаточно сложной природы. Поэтому в сложных случаях, когда есть необходимость избежать неоднозначностей, рекомендуется явно указывать тип выражений.
Сама модель типизации основана на алгоритме вывода типов выражений, который имеет своим источником механизм получения типов выражений, используемый в типизированном λ-исчислении, который был предложен в 1958 г. Х. Карри и Р. Фейсом. Далее уже́ Роджер Хиндли в 1969 г. расширил сам алгоритм и доказал, что он выводит наиболее общий тип выражения. В 1978 г. Робин Милнер независимо от Р. Хиндли доказал свойства эквивалентного алгоритма. И, наконец, в 1985 г. Луис Дамас окончательно показал, что алгоритм Милнера является законченным и может использоваться для полиморфных типов. В связи с этим алгоритм Хиндли — Милнера иногда называют также и алгоритмом Дамаса — Милнера.
Система типов определяется в модели Хиндли — Милнера следующим образом:
- Примитивные типы v{displaystyle v}
являются типами выражений.
- Параметрические переменные типов α являются типами выражений.
- Если σ1{displaystyle sigma _{1}}
и σ2{displaystyle sigma _{2}}
— типы выражений, то тип σ1→σ2{displaystyle sigma _{1}rightarrow sigma _{2}}
является типом выражений.
- Символ ⊥{displaystyle bot }
является типом выражений.
Выражения, типы которых вычисляются, определяются довольно стандартным образом:
- Константы являются выражениями.
- Переменные являются выражениями.
- Если e1{displaystyle e_{1}}
и e2{displaystyle e_{2}}
— выражения, то (e1e2{displaystyle e_{1}e_{2}}
) — выражение.
- Если v{displaystyle v}
— выражение, то λv.e{displaystyle lambda v.e}
— выражение.
Говорят, что тип σ1{displaystyle sigma _{1}}
σ1=ρ(σ2){displaystyle sigma _{1}=rho (sigma _{2})}
При этом обычно полагается, что на преобразования типов ρ{displaystyle rho }
- ρ(σ1→σ2)=ρ(σ1)→ρ(σ2){displaystyle rho (sigma _{1}rightarrow sigma _{2})=rho (sigma _{1})rightarrow rho (sigma _{2})}
- ρ(v)=v{displaystyle rho (v)=v}
Сам алгоритм вывода типов состоит из двух шагов — генерация системы уравнений и последующее решение этих уравнений.
Построение системы уравнений |
Построение системы уравнений основано на следующих правилах:
fΓv=τ{displaystyle fGamma v=tau }— в том случае, если связывание v:τ{displaystyle v:tau }
находится в Γ{displaystyle Gamma }
.
fΓ(ef)=τ{displaystyle fGamma (ef)=tau }— в том случае, если τ1=τ2→τ{displaystyle tau _{1}=tau _{2}rightarrow tau }
, где τ1=fΓe{displaystyle tau _{1}=fGamma e}
и τ2=fΓf{displaystyle tau _{2}=fGamma f}
.
fΓ(λv.e)=τ→τe{displaystyle fGamma (lambda v.e)=tau rightarrow tau _{e}}— в том случае, если τe=fΓ′e{displaystyle tau _{e}=fGamma 'e}
и Γ′{displaystyle Gamma '}
является расширением Γ{displaystyle Gamma }
В этих правилах под символом Γ{displaystyle Gamma }
Γ=v1:A1,v2:A2,…,vn:An{displaystyle Gamma =v_{1}:A_{1},v_{2}:A_{2},ldots ,v_{n}:A_{n}}
Решение системы уравнений |
Решение построенной системы уравнений основано на алгоритме унификации. Это достаточно простой алгоритм. Имеется некоторая функция u{displaystyle u}
См. также |
- Утиная типизация
- Приведение типа
Примечания |
Комментарии |
↑ поддержка добавлена в Java SE 10
Источники |
↑ Andrew W. Appel. A Critique of Standard ML. — Princeton University, revised version of CS-TR-364-92, 1992.
↑ Michał Moskal. Type Inference with Deferral. — 2005.
Ссылки |
Реализация алгоритма Хиндли-Милнера на Perl (англ.)
Archived e-mail message by Roger Hindley, explains history of type inference
Polymorphic Type Inference 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 paper by Luca Cardelli, describes algorithm, includes implementation in Modula-2
Implementation 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?) Explains Hindley-Milner, examples in Scala
http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ Модель типизации Хиндли-Милнера и пример её реализации на языке Haskell
 | Для улучшения этой статьи желательно: |
