Змі́нна ти́пу або ти́пова змі́нна в мовах програмування та теорії типів — змінна, яка може набувати значень із множини типів даних.

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

Приклад
У такому визначенні поліморфного типу «список» мовою , ідентифікатор '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
Це стає наочним за використання явного зв'язування ( або ) ти́пової змінної:
val foo: 'a 'a -> 'a
val bar: 'a 'a -> 'a
Зв'язування обмежує область дії даної змінної типу.

У класичних діалектах ML явне зв'язування ти́пових змінних є необов'язковою можливістю і більшість реалізацій його не підтримує через непотрібність — зв'язування в них здійснюється неявно при виводі типів, що стає можливим за рахунок обмежень ранніх версій системи Гіндлі — Мілнера. У повній системі F це оголошення записується як . Такий запис називають . Велика  в цьому записі означає функцію шару типів (), параметром якої є змінна типу. Після підстановки в цю змінну конкретного типу, ця функція повертає мономорфну функцію шару значень (). Пренексом називають винесене як префікс до сигнатури типу явне зв'язування змінної типу. Ранні версії системи Гіндлі — Мілнера дозволяють лише пренексну форму, тобто вимагають, щоб інстанцування ти́пової змінної певним значенням здійснювалось до звернення до функції. Це обмеження називають пренексним поліморфізмом — воно не тільки суттєво спрощує механізм перевірки узгодження типів, але й уможливлює вивід усіх або майже всіх (залежно від діалекту) типів у програмі.

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

* дія змінної типу поширюється на визначення типу: 'a, 'b 'a -> 'b -> 'a, математично такий тип записують через квантор загальності —  — тому таку змінну типу називають «універсально квантифікованою», а весь тип — «універсально поліморфним»;
* дія змінної типу поширюється тільки на частину визначення типу: 'a 'a -> ('b 'b -> 'a), математично такий тип записують через квантор існування  тому таку змінну називають «екзистенційно квантифікованою», а весь тип — «екзистенційним».

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

На практиці універсально поліморфні типи дають узагальненість типу даних, а екзистенційні — абстрактність типу даних.

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

OCaml реалізує підтримку екзистенційної квантифікації за допомогою рішення, названого «локально-абстрактними типами» ().

У специфікації 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 виділялися спеціальні підкласи змінних типу.

Змінні типу, який допускає перевірку на рівність (або змінні порівнюваного типу, ), можуть набувати значень із множини всіх типів, що допускають перевірку на рівність (). Їх використання дозволяє застосування операції порівняння на рівність об'єктів поліморфних типів. Позначаються як «a» (цифробуквений ідентифікатор, який завжди починається з двох апострофів). Цікаво, що однією з початкових цілей, заради яких розроблено класи типів, було саме узагальнення таких типових змінних зі . Вони неодноразово зазнавали критики через суттєве (і спірно виправдане) ускладнення визначення мови та реалізації компіляторів (половина сторінок Визначення містять ту чи іншу поправку). Складні абстрактні типи даних у принципі не доцільно перевіряти на рівність, оскільки такі перевірки можуть вимагати значних витрат часу. Тому з пізніших мов сімейства ML підтримка змінних типу, що допускає перевірку на рівність, виключено. У Haskell замість них використовується клас типів Eq a.

Імперативні змінні типу () забезпечували ситуативне вирішення проблеми типобезпеки, пов'язаної з наявністю побічних ефектів у мові з параметричним поліморфізмом. Ця проблема не виникає в чистих мовах (Haskell, ), але для нечистих мов (Standard ML, OCaml) поліморфізм посилань становить загрозу помилок типізації. Імперативні змінні типу входили в Визначення SML'90, але перестали мати власний сенс після того, як було придумано «обмеження значеннями» (), що стало частиною переглянутого визначення SML'97. Синтаксичну підтримку імперативних змінних типу SML'97 збережено для зворотної сумісності з написаним раніше кодом, але сучасні реалізації трактують їх ідентично аплікативним. Позначаються '_a' (цифробуквенний ідентифікатор, який завжди починається з апострофа і символу підкреслення).

Слабкі змінні типу () використовувалися в компіляторі  як альтернатива імперативним змінним типу, надаючи істотно більші можливості (точніше, менші обмеження). Позначаються '1a', '2a' і так далі (цифробуквенний ідентифікатор, що завжди починається з апострофа та цифри). Цифра, що безпосередньо йде за апострофом, показувала градацію «слабкості» змінної типу. Як і імперативні змінні типу, нині трактуються ідентично аплікативним.

Примітки


Література
* 
* 

Посилання
* 
* 
* 
* 
* 



