Переменная типа - NiNa.Az

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

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

Пример

В следующем определении полиморфного типа «список» на языке Standard ML, идентификатор 'a (читается «альфа») является переменной типа:

datatype 'a list = nil | :: of 'a * 'a list 

При использовании этого полиморфного типа, в ти́повую переменную подставляется конкретный тип, так что в программе может быть сформировано множество мономорфных типов: string list, int list, int list list и так далее. При такой подстановке, вместо каждого упоминания переменной типа подставляется один и тот же тип. Полученная информация о типах используется для верификации и оптимизации программы, после чего обычно стирается, так что один и тот же целевой код обрабатывает объекты изначально разных типов (но существуют и исключения из этого правила, в частности, в MLton).

Если полиморфный тип параметризован несколькими переменными типа, то подставляемые в них типы могут быть как разными, так и идентичными, но правило подстановки соблюдается. Например, если такой тип:

datatype ('a,'b) t = Single of 'a | Double of 'a * 'a | Pair of 'a * 'b 

инстанцировать следующим образом:

type t_ir = (int, real) t 

то Single(4), Double(4,5) и Pair(4,5.0) будут допустимыми значениями типа t_ir, а попытка построить значение Single(5.0) приведёт к ошибке типизации, поскольку параметр 'a получил значение «int».

Связывание и квантификация

Область действия всякой ти́повой переменной привязывается к определённому контексту. В следующем примере идентификатор 'a используется в двух сигнатурах независимо, то есть не означает требование равенства фактически подставляемых типов между определениями:

val foo: 'a -> 'a val bar: 'a -> 'a 

Это становится наглядным при использовании явного связывания (explicit scoping или explicit bounding) ти́повой переменной:

val foo: ['a] 'a -> 'a val bar: ['a] 'a -> 'a 

Связывание ограничивает область действия данной переменной типа.

В классических диалектах ML явное связывание ти́повых переменных является необязательной возможностью и большинством реализаций не поддерживается за ненадобностью — связывание в них осуществляется неявно при выведении типов, что становится возможным за счёт ограничений ранних версий системы Хиндли — Милнера. В полной системе F это объявление записывается как ${\displaystyle \Lambda \alpha .~\lambda x^{\alpha }.~x}$. Такая запись называется ^[англ.]. Заглавная ${\displaystyle \Lambda }$ в этой записи означает функцию слоя типов (type-level function), параметром которой и является переменная типа. После подстановки в эту переменную конкретного типа, эта функция возвращает мономорфную функцию слоя значений (value-level function). Пренексом называется вынесенное в качестве префикса к сигнатуре типа явное связывание переменной типа. Ранние версии системы Хиндли — Милнера разрешают только пренексную форму, то есть требуют, чтобы инстанцирование ти́повой переменной определённым значением было произведено до необходимости обращения к функции. Это ограничение называется пренексным полиморфизмом — оно не только существенно упрощает механизм проверки согласования типов, но и делает возможным выведение всех или почти всех (в зависимости от диалекта) типов в программе.

Простейшее связывание ти́повых переменных называется их квантификацией. Выделяются два случая:

• действие переменной типа распространяется на всё определение типа: ['a, 'b] 'a -> 'b -> 'a, математически такой тип записывается через квантор всеобщности — ${\displaystyle \forall a.~\forall b.~a\rightarrow b\rightarrow a}$ — поэтому такая переменная типа называется «универсально квантифицированной», а весь тип — «универсально полиморфным»;
• действие переменной типа распространяется только на часть определения типа: ['a] 'a -> (['b] 'b -> 'a), математически такой тип записывается через квантор существования — ${\displaystyle \forall a.~\exists b.~a\rightarrow b\rightarrow a}$ — поэтому такая переменная называется «экзистенциально квантифицированной», а весь тип — «экзистенциальным».

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

На практике, универсально полиморфные типы дают обобщённость типа данных, а экзистенциальные — абстрактность типа данных.

В языке Haskell различают несколько режимов (доступных в виде расширений языка): режим Rank2Types разрешает лишь некоторые формы экзистенциальных типов, открывающие полиморфизм не выше 2-го ранга, для которого выведение типов ещё разрешимо; режим RankNTypes разрешает перемещать универсальный квантор (forall a) внутрь функциональных типов, входящих в состав более сложных сигнатур, режим ImpredicativeTypes разрешает произвольные экзистенциальные типы.

OCaml реализует поддержку экзистенциальной квантификации посредством решения, названного «локально-абстрактными типами» (locally abstract types).

В спецификации Standard ML для некоторых встроенных операций определена особая квантификация. Её синтаксис не регламентирован и различается в реализациях языка (чаще всего просто скрывается). Например, сигнатура встроенной операции сложения может упрощённо выглядеть примерно следующим образом:

val + : [int, word, real] 'a * 'a -> 'a 

Эта семантика реализует примитивную форму ad-hoc-полиморфизма — объединение нескольких физически различных операций сложения под единым идентификатором «+». Разработчики OCaml отказались от такого решения, полностью убрав ad-hoc-полиморфизм из языка (в более поздних версиях появились обобщённые алгебраические типы данных).

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

Впервые это расширение было реализовано в основе языка Haskell, например, операция сравнения на равенство имеет в нём следующую ^[англ.]:

(==) :: (Eq a) => a -> a -> Bool 

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

Специальные переменные типа

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

Кроме этого, на протяжении истории развития ML выделялись специальные подклассы переменных типа.

Переменные типа, допускающего проверку на равенство (или переменные сравниваемого типа, equality type variables) — могут принимать значения из множества всех (англ. equality types). Их использование разрешает применение операции сравнения на равенство к объектам полиморфных типов. Обозначаются как «''a» (цифробуквенный идентификатор, всегда начинающийся с двух апострофов). Интересно, что одной из первоначальных целей, ради которых были разработаны классы типов, было именно обобщение таких ти́повых переменных из Standard ML. Они неоднократно подвергалась критике из-за существенного (и спорно оправданного) усложнения определения языка и реализации компиляторов (половина страниц Определения содержат ту или иную поправку на них). Сложные абстрактные типы данных в принципе не целесообразно проверять на равенство, так как такие проверки могут требовать существенных затрат времени. Поэтому из более поздних языков семейства ML поддержка переменных типа, допускающего проверку на равенство, была исключена. В Haskell вместо них используется класс типов Eq a.

Императивные переменные типа (imperative type variables) обеспечивали ситуативное решение проблемы типобезопасности, связанной с наличием побочных эффектов в языке с параметрическим полиморфизмом. Этой проблемы не возникает в чистых языках (Haskell, Clean), но для нечистых языков (Standard ML, OCaml) полиморфизм ссылок представляет угрозу ошибок типизации. Императивные переменные типа входили в Определение SML’90, но перестали иметь собственный смысл после того как было придумано «ограничение значениями» (value restriction), ставшее частью пересмотренного определения SML’97. Синтаксическая поддержка императивных переменных типа в SML’97 была сохранена для обратной совместимости с написанным ранее кодом, но современные реализации трактуют их идентично аппликативным. Обозначаются «'_a» (цифробуквенный идентификатор, всегда начинающийся с апострофа и символа подчёркивания).

Слабые переменные типа (weak type variables) использовались в компиляторе ^[англ.] в качестве альтернативы императивным переменным типа, предоставляя существенно большие возможности (точнее, меньшие ограничения). Обозначаются «'1a», «'2a» и так далее (цифробуквенный идентификатор, всегда начинающийся с апострофа и цифры). Цифра, непосредственно идущая за апострофом, показывала градацию «слабости» переменной типа. Как и императивные переменные типа, ныне трактуются идентично аппликативным.

Примечания

1. ML2000, 1999.
2. Здесь для явного связывания (explicit binding) ти́повой переменной используется текущий синтаксис, принятый в проекте successor ML: ['a]. Из-за того, что в Haskell этот синтаксис был назначен в качестве синтаксического сахара над типом List, для объявления ти́повых переменных в нём было введено ключевое слово forall.
3. MacQueen - TypeChecking.
4. MLton - Scoping.
5. haskell_existentials.
6. Cardelli, Wegner, 1985.
7. haskell_rankNtypes.
8. haskell_impredicative_types.
9. OCaml extenstions. 7.13 Locally abstract types
10. Philip Wadler, Stephen Blott. How to make ad-hoc polymorphism less ad hoc. — 1988. Архивировано 11 марта 2016 года.
11. Andrew W. Appel. A Critique of Standard ML. — Princeton University, revised version of CS-TR-364-92, 1992. Архивировано 5 марта 2016 года.

Литература

• Luca Cardelli, Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism. — , 1985. — С. 471—523. — ISSN 0360-0300.
• Dave MacQueen. SML'97 Conversion Guide. 1.1. Types and Type Checking.

Ссылки

• Haskell-Wiki: Existential types  (неопр.).
• Haskell-Wiki: Rank-N types  (неопр.).
• Haskell-Wiki: Impredicative types  (неопр.).
• Scoping type variables in Standard ML  (неопр.).
• The ML2000 Working Group. Principles and a Preliminary Design for ML2000. — 1999.