Просмотр кода страницы Переменная типа

'''Переменная типа''' (''ти́повая переменная'') в [[язык программирования|языках программирования]] и [[Теория типов|теории типов]] — [[переменная (математика)|переменная]], которая может принимать значение из множества [[тип данных|типов данных]].

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

== Пример ==
В следующем определении [[полиморфизм типов|полиморфного типа]] «[[список (программирование)|список]]» на языке {{nobr|[[Standard ML]]}}, идентификатор <code>'a</code> (читается «альфа») является переменной типа{{#tag:ref|Здесь для явного связывания ({{lang-en2|explicit binding}}) ти́повой переменной используется текущий синтаксис, принятый в проекте {{nobr|successor ML}}{{sfn|ML2000|1999}}: <code>['a]</code>. Из-за того, что в [[Haskell]] этот синтаксис был назначен в качестве [[синтаксический сахар|синтаксического сахара]] над типом <code>[[список (программирование)|List]]</code>, для объявления ти́повых переменных в нём было введено [[ключевое слово]] <code>forall</code>.}}:
<source lang=sml>
datatype 'a list = nil | :: of 'a * 'a list
</source>
При использовании этого [[полиморфизм типов|полиморфного типа]], в ти́повую переменную подставляется конкретный тип, так что в программе может быть сформировано множество мономорфных типов: <code>string list</code>, <code>int list</code>, <code>int list list</code> и так далее. При такой подстановке, вместо каждого упоминания переменной типа подставляется один и тот же тип. Полученная информация о типах используется для [[типобезопасность|верификации]] и [[оптимизирующий компилятор|оптимизации]] программы, после чего обычно стирается, так что один и тот же целевой код обрабатывает объекты изначально разных типов (но существуют и исключения из этого правила, в частности, в [[MLton]]).

Если полиморфный тип параметризован несколькими переменными типа, то подставляемые в них типы могут быть как разными, так и идентичными, но правило подстановки соблюдается. Например, если такой тип:
<source lang=sml>
datatype ('a,'b) t = Single of 'a | Double of 'a * 'a | Pair of 'a * 'b
</source>
инстанцировать следующим образом:
<source lang=sml>
type t_ir = (int, real) t
</source>
то <code>Single(4)</code>, <code>Double(4,5)</code> и <code>Pair(4,5.0)</code> будут допустимыми значениями типа <code>t_ir</code>, а попытка построить значение <code>Single(5.0)</code> приведёт к [[ошибка типизации|ошибке типизации]], поскольку параметр <code>'a</code> получил значение «<code>int</code>».

== Связывание и квантификация ==
[[Область видимости|Область действия]] всякой ти́повой переменной привязывается к определённому контексту{{sfn|MacQueen - TypeChecking}}{{sfn|MLton - Scoping}}. В следующем примере идентификатор <code>'a</code> используется в двух сигнатурах независимо, то есть не означает требование равенства фактически подставляемых типов между определениями:
<source lang=sml>
val foo: 'a -> 'a
val bar: 'a -> 'a
</source>
Это становится наглядным при использовании явного связывания ({{lang-en2|explicit scoping}} или {{lang-en2|explicit bounding}}) ти́повой переменной:
<source lang=sml>
val foo: ['a] 'a -> 'a
val bar: ['a] 'a -> 'a
</source>
Связывание ограничивает область действия данной переменной типа.

В классических диалектах ML явное связывание ти́повых переменных является необязательной возможностью и большинством реализаций не поддерживается за ненадобностью — связывание в них осуществляется ''неявно'' при [[выведение типов|выведении типов]], что становится возможным за счёт ограничений ранних версий [[Система типов Хиндли — Милнера|системы Хиндли — Милнера]]. В полной [[Система F|системе F]] это объявление записывается как <math>\Lambda\alpha.~\lambda x^\alpha.~x</math>. Такая запись называется {{iw|Пренексная нормальная форма|пренексной нормальной формой|en|Prenex normal form}}. Заглавная <math>\Lambda</math> в этой записи означает функцию слоя типов ({{lang-en2|type-level function}}), параметром которой и является переменная типа. После подстановки в эту переменную конкретного типа, эта функция возвращает мономорфную функцию слоя значений ({{lang-en2|value-level function}}). Пренексом называется вынесенное в качестве префикса к сигнатуре типа явное связывание переменной типа. Ранние версии системы Хиндли — Милнера разрешают только пренексную форму, то есть требуют, чтобы инстанцирование ти́повой переменной определённым значением было произведено до необходимости обращения к функции. Это ограничение называется [[параметрический полиморфизм#Пренексный полиморфизм|пренексным полиморфизмом]] — оно не только существенно упрощает механизм [[проверка согласования типов|проверки согласования типов]], но и делает возможным [[выведение типов|выведение]] всех или почти всех (в зависимости от диалекта) типов в программе.

Простейшее связывание ти́повых переменных называется их [[квантификация|квантификацией]]. Выделяются два случая:
* действие переменной типа распространяется на всё определение типа: <code>['a, 'b] 'a -> 'b -> 'a</code><!-- стилистическое решение, которое в данном случае лучше — <source> ломает табуляцию, что для перечисления нежелательно; с другой - необходимо наглядное сопоставление сигнатур типов -->, математически такой тип записывается через [[квантор всеобщности]] — <math>\forall a. ~\forall b. ~a \rightarrow b \rightarrow a</math> — поэтому такая переменная типа называется «универсально квантифицированной», а весь тип — «универсально полиморфным»;
* действие переменной типа распространяется только на часть определения типа: <code>['a] 'a -> (['b] 'b -> 'a)</code>, математически такой тип записывается через [[квантор существования]] — <math>\forall a. ~\exists b. ~a \rightarrow b \rightarrow a </math> — поэтому такая переменная называется «экзистенциально квантифицированной», а весь тип — «экзистенциальным». 

Далеко не во всех случаях «превращение» универсально полиморфного типа в экзистенциальный даёт применимый на практике тип или заметные отличия от универсального полиморфизма, но в определённых случаях использование [[экзистенциальный тип|экзистенциальных типов]] поднимает [[параметрический полиморфизм]] на [[объект первого класса|первоклассный]] уровень, т.е. позволяет передавать полиморфные функции без связывания в качестве параметров другим функциям (см. [[полиморфизм первого класса]]). Классическим примером является реализация гетерогенного списка (см. викиучебник). [[Явная типизация|Явное аннотирование типов]] в этом случае становится обязательным, т.к. [[выведение типов]] для полиморфизма выше ранга 2 [[алгоритмическая разрешимость|алгоритмически неразрешимо]]{{sfn|haskell_existentials}}.

На практике, универсально полиморфные типы дают [[полиморфизм типов|обобщённость типа данных]], а экзистенциальные — [[абстрактный тип данных|абстрактность типа данных]]{{sfn|Cardelli, Wegner|1985}}.

В языке Haskell различают несколько режимов (доступных в виде расширений языка): режим <tt>Rank2Types</tt> разрешает лишь некоторые формы экзистенциальных типов, открывающие полиморфизм не выше 2-го ранга, для которого [[выведение типов]] ещё разрешимо; режим <tt>RankNTypes</tt> разрешает перемещать [[Квантор всеобщности|универсальный квантор]] (<code>forall a</code>) внутрь [[функциональный тип|функциональных типов]], входящих в состав более сложных сигнатур{{sfn|haskell_rankNtypes}}, режим <tt>ImpredicativeTypes</tt> разрешает произвольные экзистенциальные типы{{sfn|haskell_impredicative_types}}.

[[OCaml]] реализует поддержку экзистенциальной квантификации посредством решения, названного «локально-абстрактными типами» ({{lang-en2|locally abstract types}})<ref>[http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec228 OCaml extenstions. 7.13 Locally abstract types]</ref>.

В спецификации [[Standard ML]] для некоторых встроенных операций определена особая квантификация. Её синтаксис не регламентирован и различается в реализациях языка (чаще всего просто скрывается). Например, сигнатура встроенной операции сложения может упрощённо выглядеть примерно следующим образом:
<source lang=sml>
val + : [int, word, real] 'a * 'a -> 'a
</source>
Эта семантика реализует примитивную форму [[ad-hoc-полиморфизм]]а — объединение нескольких физически различных операций сложения под единым идентификатором «<code>+</code>». Разработчики [[OCaml]] отказались от такого решения, полностью убрав ad-hoc-полиморфизм из языка (в более поздних версиях появились [[обобщённый алгебраический тип данных|обобщённые алгебраические типы данных]]).

В конце [[1980-е годы|1980-х]] появилось расширение [[Система типов Хиндли — Милнера|Хиндли — Милнера]], предоставляющее возможность ограничивать по необходимости диапазон значений для всякой ти́повой переменной во вновь определяемых типах — [[Класс типов|классы типов]]. Класс типов строже ограничивает допустимые [[Система F#Контексты типизации и утверждение типизации|контексты типизации]], разрешая инстанцирование ти́повой переменной лишь типами, принадлежащими явно указанному классу.

Впервые это расширение было реализовано в основе языка [[Haskell]], например, операция [[Равенство (математика)|сравнения на равенство]] имеет в нём следующую {{iw|Сигнатура типа|сигнатуру|en|Type signature}}:
<source lang=haskell>
(==) :: (Eq a) => a -> a -> Bool
</source>

Проект языка следующего поколения — successor ML{{sfn|ML2000|1999}} — отказывается от необходимости [[выведение типов|выведения типов]], опираясь на [[Явная типизация|явное (манифестное) аннотирование типов]] (в том числе явное связывание переменных типа), что обеспечивает непосредственную поддержку полной системы F с [[полиморфизм первого класса|полиморфизмом первого класса]] и рядом расширений, в том числе {{iw|Выделение подтипов данных|иерархии подтипов|en|Subtyping}} и [[экзистенциальный тип|экзистенциальных типов]]{{sfn|ML2000|1999}}.

== Специальные переменные типа ==
Основным классом переменных типа, используемым во всех языках семейства [[ML]], являются аппликативные переменные типа, могут принимать значения из множества всех допустимых в конкретном языке типов. В классических диалектах они синтаксически обозначаются как «<code>'a</code>» (цифробуквенный идентификатор, всегда начинающийся с одного [[апостроф]]а); в [[Haskell]] как «<code>a</code>» (цифробуквенный идентификатор, всегда начинающийся со строчной буквы).

Кроме этого, на протяжении истории развития [[ML]] выделялись специальные подклассы<!-- термин «subclass» используется в Определении SML --> переменных типа.

Переменные типа, допускающего проверку на равенство (или переменные сравниваемого типа, {{lang-en2|equality type variables}}) — могут принимать значения из множества всех [[Тип, допускающий проверку на равенство|типов, допускающих проверку на равенство]] ({{lang-en|equality types}}). Их использование разрешает применение операции [[Равенство (математика)|сравнения на равенство]] к объектам полиморфных типов. Обозначаются как «<code><nowiki>''</nowiki>a</code>» (цифробуквенный идентификатор, всегда начинающийся с двух [[апостроф]]ов). Интересно, что одной из первоначальных целей, ради которых были разработаны [[Класс типов|классы типов]], было именно обобщение таких ти́повых переменных из {{nobr|[[Standard ML]]}}<ref>{{статья
| заглавие = How to make ad-hoc polymorphism less ad hoc
| автор = Philip Wadler, Stephen Blott.
| ссылка = http://homepages.inf.ed.ac.uk/wadler/papers/class/class.ps
| год = 1988
| archivedate = 2016-03-11
| archiveurl = https://web.archive.org/web/20160311163323/http://homepages.inf.ed.ac.uk/wadler/papers/class/class.ps
}}</ref>. Они неоднократно подвергалась критике из-за существенного (и спорно оправданного) усложнения определения языка и реализации компиляторов (половина страниц Определения содержат ту или иную поправку на них)<ref>{{статья
|заглавие = A Critique of Standard ML
|автор = Andrew W. Appel
|издательство = Princeton University, revised version of CS-TR-364-92
|год = 1992
|ссылка = http://www.cs.princeton.edu/research/techreps/TR-364-92
|ref = Appel - A Critique of Standard ML
|archivedate = 2016-03-05
|archiveurl = https://web.archive.org/web/20160305071636/http://www.cs.princeton.edu/research/techreps/TR-364-92
}}</ref>. Сложные абстрактные типы данных в принципе не целесообразно проверять на равенство, так как такие проверки могут требовать существенных затрат времени. Поэтому из более поздних языков семейства [[ML]] поддержка переменных типа, допускающего проверку на равенство, была исключена. В Haskell вместо них используется [[класс типов]] <code>Eq a</code>.

Императивные переменные типа ({{lang-en2|imperative type variables}}) обеспечивали ситуативное решение проблемы [[типобезопасность|типобезопасности]], связанной с наличием [[побочный эффект (программирование)|побочных эффектов]] в языке с [[параметрический полиморфизм|параметрическим полиморфизмом]]. Этой проблемы не возникает в чистых языках ([[Haskell]], [[Clean]]), но для нечистых языков ([[Standard ML]], [[OCaml]]) полиморфизм [[ссылка (программирование)|ссылок]] представляет угрозу [[ошибка типизации|ошибок типизации]]{{sfn|MacQueen - TypeChecking}}{{sfn|MLton - Scoping}}. Императивные переменные типа входили в Определение SML’90, но перестали иметь собственный смысл после того как было придумано «ограничение значениями» ({{lang-en2|value restriction}}), ставшее частью пересмотренного определения SML’97. Синтаксическая поддержка императивных переменных типа в SML’97 была сохранена для обратной совместимости с написанным ранее кодом, но современные реализации трактуют их идентично аппликативным. Обозначаются «<code>'_a</code>» (цифробуквенный идентификатор, всегда начинающийся с апострофа и символа подчёркивания){{sfn|MacQueen - TypeChecking}}.

Слабые переменные типа ({{lang-en2|weak type variables}}) использовались в компиляторе {{iw|SML/NJ}} в качестве альтернативы императивным переменным типа, предоставляя существенно большие возможности (точнее, меньшие ограничения). Обозначаются «<code>'1a</code>», «<code>'2a</code>» и так далее (цифробуквенный идентификатор, всегда начинающийся с [[апостроф]]а и цифры). Цифра, непосредственно идущая за апострофом, показывала градацию «слабости» переменной типа. Как и императивные переменные типа, ныне трактуются идентично аппликативным.{{sfn|MacQueen - TypeChecking}}

== Примечания ==
{{примечания}}

== Литература ==
* {{статья
| автор = Luca Cardelli, Peter Wegner
| заглавие = On Understanding Types, Data Abstraction, and Polymorphism
| издательство = [[ACM Computing Surveys]]
| год = 1985
| ссылка = http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf
| страницы = 471—523
| issn = 0360-0300
| ref = Cardelli, Wegner
}}
* {{статья
| автор = Dave MacQueen.
| заглавие = SML'97 Conversion Guide. 1.1. Types and Type Checking
| издательство =
| год =
| ссылка = http://www.smlnj.org/doc/Conversion/types.html
| страницы =
| issn =
| ref = MacQueen - TypeChecking
}}

== Ссылки ==
* {{Cite web
| url = https://wiki.haskell.org/Existential_type
| title = Haskell-Wiki: Existential types
| ref = haskell_existentials
}}
* {{Cite web
| url = https://wiki.haskell.org/Rank-N_types
| title = Haskell-Wiki: Rank-N types
| ref = haskell_rankNtypes
}}
* {{Cite web
| url = https://wiki.haskell.org/Impredicative_types
| title = Haskell-Wiki: Impredicative types
| ref = haskell_impredicative_types
}}
* {{Cite web
| url = http://www.mlton.org/TypeVariableScope
| title = Scoping type variables in Standard ML
| ref = MLton - Scoping
}}
* {{статья
| заглавие = Principles and a Preliminary Design for ML2000
| автор = The ML2000 Working Group.
| ссылка = http://flint.cs.yale.edu/flint/publications/ml2000.pdf
| год = 1999
| ref = ML2000
}}

{{Типы данных}}

[[Категория:Теория типов]]
[[Категория:Типы данных]]
[[Категория:Функциональное программирование]]