Перегляд вихідного коду сторінки Змінна типу

'''Змі́нна ти́пу''' або '''ти́пова змі́нна''' в [[Мова програмування|мовах програмування]] та [[Теорія типів|теорії типів]]&nbsp;— [[змінна]], яка може набувати значень із множини [[Тип даних|типів даних]].

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

== Приклад ==
У такому визначенні [[Поліморфізм типів|поліморфного типу]] «[[Список (абстрактний тип даних)|список]]» мовою {{Nobr|[[Standard ML]]}}, ідентифікатор <code>'a</code> (читається «альфа») є змінною типу{{#tag:ref|Тут для явного зв'язування ({{lang-en|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> і&nbsp;т.&nbsp;д. За такої підстановки замість кожної згадки змінної типу підставляється один і той самий тип. Отримана інформація про типи використовується для [[Безпека типів|верифікації]] та [[Оптимізувальний компілятор|оптимізації]] програми, після чого зазвичай стирається, тому один і той самий цільовий код обробляє об'єкти спочатку різних типів (але існують і винятки з цього правила, зокрема, в [[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 явне зв'язування ти́пових змінних є необов'язковою можливістю і більшість реалізацій його не підтримує через непотрібність&nbsp;— зв'язування в них здійснюється ''неявно'' при [[Вивід типів|виводі типів]], що стає можливим за рахунок обмежень ранніх версій [[Вивід типів|системи Гіндлі&nbsp;— Мілнера]]. У повній [[Система F|системі F]] це оголошення записується як <math>\Lambda\alpha.~\lambda x^\alpha.~x</math>. Такий запис називають {{Не перекладено|Пренексна нормальна форма|пренексною нормальною формою|en|Prenex normal form}}. Велика <math>\Lambda</math> в цьому записі означає функцію шару{{Уточнити}} типів ({{Lang-en2|type-level function}}), параметром якої є змінна типу. Після підстановки в цю змінну конкретного типу, ця функція повертає мономорфну функцію шару значень ({{Lang-en2|value-level function}}). Пренексом називають винесене як префікс до сигнатури типу явне зв'язування змінної типу. Ранні версії системи Гіндлі&nbsp;— Мілнера дозволяють лише пренексну форму, тобто вимагають, щоб інстанцування ти́пової змінної певним значенням здійснювалось до звернення до функції. Це обмеження називають [[Параметричний поліморфізм|пренексним поліморфізмом]]&nbsp;— воно не тільки суттєво спрощує механізм [[Перевірка узгодження типів|перевірки узгодження типів]], але й уможливлює [[Вивід типів|вивід]] усіх або майже всіх (залежно від діалекту) типів у програмі.

Найпростіше зв'язування ти́пових змінних називають їх [[Квантор|квантифікацією]]. Виділяють два випадки:

* дія змінної типу поширюється на визначення типу: <code>['a, 'b] 'a -> 'b -> 'a</code>, математично такий тип записують через [[квантор загальності]]&nbsp;— <math>\forall a. ~\forall b. ~a \rightarrow b \rightarrow a</math>&nbsp;— тому таку змінну типу називають «універсально квантифікованою», а весь тип&nbsp;— «універсально поліморфним»;
* дія змінної типу поширюється тільки на частину визначення типу: <code>['a] 'a -> (['b] 'b -> 'a)</code>, математично такий тип записують через [[квантор існування]] <math>\forall a. ~\exists b. ~a \rightarrow b \rightarrow a </math> тому таку змінну називають «екзистенційно квантифікованою», а весь тип&nbsp;— «екзистенційним».

Далеко не завжди «перетворення» універсально поліморфного типу на екзистенційний дає застосовний практично тип чи помітні відмінності від універсального поліморфізму, але в певних випадках використання [[Система типізації|екзистенційних типів]] піднімає [[параметричний поліморфізм]] на [[Об'єкт першого класу|першокласний]] рівень, тобто, дозволяє передавати поліморфні функції без зв'язування як параметри іншим функціям (див. [[поліморфізм першого класу]]). Класичним прикладом є реалізація гетерогенного списку (див. вікіпідручник). [[Явна типізація|Явне призначення типів]] у цьому разі стає обов'язковим, оскільки [[вивід типів]] для поліморфізму вище від рангу 2 [[Алгоритмічна розв'язність|алгоритмічно нерозв'язний]]{{Sfn|haskell_existentials}}.

На практиці універсально поліморфні типи дають [[Поліморфізм типів|узагальненість типу даних]], а екзистенційні&nbsp;— [[Абстрактний тип даних|абстрактність типу даних]]{{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}}.

[[Objective Caml|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-поліморфізму]]&nbsp;— об'єднання кількох фізично різних операцій додавання під єдиним ідентифікатором «<code>+</code>». Розробники [[Objective Caml|OCaml]] відмовилися від такого рішення, повністю прибравши ad-hoc-поліморфізм із мови (у пізніших версіях з'явилися [[Узагальнений алгебричний тип даних|узагальнені алгебричні типи даних]]).

Наприкінці [[1980-ті|1980-х]] з'явилося розширення [[Вивід типів|Гіндлі&nbsp;— Мілнера]], що надає можливість обмежувати, за необхідності, діапазон значень для будь-якої ти́пової змінної в нововизначених типах&nbsp;— [[Поліморфізм (програмування)|класи типів]]. Клас типів суворіше обмежує допустимі [[Система F|контексти типізації]], дозволяючи інстанцування ти́пової змінної лише типами, що належать явно зазначеному класу.

Вперше це розширення реалізовано в основі мови [[Haskell]], наприклад, операція [[Відношення рівності|порівняння на рівність]] має в ньому таку [[Сигнатура типу|сигнатуру]]:<source lang="haskell">
(==) :: (Eq a) => a -> a -> Bool
</source>Проєкт мови наступного покоління&nbsp;— successor ML{{Sfn|ML2000|1999}}&nbsp;— відмовляється від необхідності [[Вивід типів|виводу типів]], спираючись на [[Явна типізація|явне (маніфестне) анотування типів]] (зокрема, явне зв'язування змінних типу), що забезпечує безпосередню підтримку повної системи F з [[Поліморфізм першого класу|поліморфізмом першого класу]] та низкою розширень, у тому числі {{Не перекладено|Виділення підтипів даних|ієрархії підтипів|en|Subtyping}} та [[Система типізації|екзистенційних типів]]{{Sfn|ML2000|1999}}.

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

Крім цього, з розвитком [[ML]] виділялися спеціальні підкласи змінних типу.

Змінні типу, який допускає перевірку на рівність (або змінні порівнюваного типу, {{Lang-en2|equality type variables}}), можуть набувати значень із множини всіх [[Тип, що допускає перевірку на рівність|типів, що допускають перевірку на рівність]] ({{Lang-en|equality types}}). Їх використання дозволяє застосування операції [[Відношення рівності|порівняння на рівність]] об'єктів поліморфних типів. Позначаються як «<code><nowiki>''</nowiki>a</code>» (цифробуквений ідентифікатор, який завжди починається з двох [[апостроф]]ів). Цікаво, що однією з початкових цілей, заради яких розроблено [[Поліморфізм (програмування)|класи типів]], було саме узагальнення таких типових змінних зі {{Nobr|[[Standard ML]]}}<ref>{{Стаття|title=How to make ad-hoc polymorphism less ad hoc|author=Philip Wadler, Stephen Blott.|url=http://homepages.inf.ed.ac.uk/wadler/papers/class/class.ps|date=1988}}</ref>. Вони неодноразово зазнавали критики через суттєве (і спірно виправдане) ускладнення визначення мови та реалізації компіляторів (половина сторінок Визначення містять ту чи іншу поправку)<ref>{{Стаття|title=A Critique of Standard ML|author=Andrew W. Appel|publisher=Princeton University, revised version of CS-TR-364-92|date=1992|url=http://www.cs.princeton.edu/research/techreps/TR-364-92|ref=Appel - A Critique of Standard ML}}</ref>. Складні абстрактні типи даних у принципі не доцільно перевіряти на рівність, оскільки такі перевірки можуть вимагати значних витрат часу. Тому з пізніших мов сімейства [[ML]] підтримка змінних типу, що допускає перевірку на рівність, виключено. У Haskell замість них використовується [[Поліморфізм (програмування)|клас типів]] <code>Eq a</code>.

Імперативні змінні типу ({{Lang-en2|imperative type variables}}) забезпечували ситуативне вирішення проблеми [[Безпека типів|типобезпеки]], пов'язаної з наявністю [[Побічний ефект (програмування)|побічних ефектів]] у мові з [[Параметричний поліморфізм|параметричним поліморфізмом]]. Ця проблема не виникає в чистих мовах ([[Haskell]], {{Нп|Clean|3=en|4=Clean (programming language)}}), але для нечистих мов ([[Standard ML]], [[Objective Caml|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}}) використовувалися в компіляторі {{Не перекладено|SML/NJ}} як альтернатива імперативним змінним типу, надаючи істотно більші можливості (точніше, менші обмеження). Позначаються <code>'1a'</code>, <code>'2a'</code> і так далі (цифробуквенний ідентифікатор, що завжди починається з [[апостроф]]а та цифри). Цифра, що безпосередньо йде за апострофом, показувала градацію «слабкості» змінної типу. Як і імперативні змінні типу, нині трактуються ідентично аплікативним{{Sfn|MacQueen - TypeChecking}}.

== Примітки ==
{{Reflist}}

== Література ==
* {{Стаття|author=Luca Cardelli, Peter Wegner|title=On Understanding Types, Data Abstraction, and Polymorphism|publisher=[[ACM Computing Surveys]]|рік=1985|url=http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf|pages=471—523|issn=0360-0300|ref=Cardelli, Wegner}}
* {{Стаття|author=Dave MacQueen.|title=SML'97 Conversion Guide. 1.1. Types and Type Checking|publisher=|date=|url=http://www.smlnj.org/doc/Conversion/types.html|pages=|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}}
* {{Стаття|title=Principles and a Preliminary Design for ML2000|author=The ML2000 Working Group.|url=http://flint.cs.yale.edu/flint/publications/ml2000.pdf|рік=1999|ref=ML2000}}
{{Типи даних}}
[[Категорія:Функційне програмування]]
[[Категорія:Типи даних]]
[[Категорія:Теорія типів]]