Змінна типу

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

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

Приклад

У такому визначенні поліморфного типу «список» мовою Шаблон:Nobr, ідентифікатор '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».

Зв'язування та квантифікація

Область дії будь-якої ти́пової змінної прив'язується до певного контекстуШаблон:SfnШаблон:Sfn. У наступному прикладі ідентифікатор 'a використовується в двох сигнатурах незалежно, тобто не означає вимоги рівності типів, що фактично підставляються між визначеннями:

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

Це стає наочним за використання явного зв'язування (Шаблон:Lang-en2 або Шаблон:Lang-en2) ти́пової змінної:

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

Зв'язування обмежує область дії даної змінної типу.

У класичних діалектах ML явне зв'язування ти́пових змінних є необов'язковою можливістю і більшість реалізацій його не підтримує через непотрібність — зв'язування в них здійснюється неявно при виводі типів, що стає можливим за рахунок обмежень ранніх версій системи Гіндлі — Мілнера. У повній системі F це оголошення записується як $\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.x$. Такий запис називають Шаблон:Не перекладено. Велика $\mathrm{\Lambda }$ в цьому записі означає функцію шаруШаблон:Уточнити типів (Шаблон:Lang-en2), параметром якої є змінна типу. Після підстановки в цю змінну конкретного типу, ця функція повертає мономорфну функцію шару значень (Шаблон:Lang-en2). Пренексом називають винесене як префікс до сигнатури типу явне зв'язування змінної типу. Ранні версії системи Гіндлі — Мілнера дозволяють лише пренексну форму, тобто вимагають, щоб інстанцування ти́пової змінної певним значенням здійснювалось до звернення до функції. Це обмеження називають пренексним поліморфізмом — воно не тільки суттєво спрощує механізм перевірки узгодження типів, але й уможливлює вивід усіх або майже всіх (залежно від діалекту) типів у програмі.

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

• дія змінної типу поширюється на визначення типу: ['a, 'b] 'a -> 'b -> 'a, математично такий тип записують через квантор загальності — $\mathrm{\forall }a.\mathrm{\forall }b.a\to b\to a$ — тому таку змінну типу називають «універсально квантифікованою», а весь тип — «універсально поліморфним»;
• дія змінної типу поширюється тільки на частину визначення типу: ['a] 'a -> (['b] 'b -> 'a), математично такий тип записують через квантор існування $\mathrm{\forall }a.\mathrm{\exists }b.a\to b\to a$ тому таку змінну називають «екзистенційно квантифікованою», а весь тип — «екзистенційним».

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

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

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

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

У специфікації Standard ML для деяких вбудованих операцій визначено особливу квантифікацію. Її синтаксис не регламентовано, він різниться в реалізаціях мови (найчастіше просто приховується). Наприклад, сигнатура вбудованої операції додавання може спрощено виглядати приблизно так:

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

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

Наприкінці 1980-х з'явилося розширення Гіндлі — Мілнера, що надає можливість обмежувати, за необхідності, діапазон значень для будь-якої ти́пової змінної в нововизначених типах — класи типів. Клас типів суворіше обмежує допустимі контексти типізації, дозволяючи інстанцування ти́пової змінної лише типами, що належать явно зазначеному класу.

Вперше це розширення реалізовано в основі мови Haskell, наприклад, операція порівняння на рівність має в ньому таку сигнатуру:

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

Проєкт мови наступного покоління — successor MLШаблон:Sfn — відмовляється від необхідності виводу типів, спираючись на явне (маніфестне) анотування типів (зокрема, явне зв'язування змінних типу), що забезпечує безпосередню підтримку повної системи F з поліморфізмом першого класу та низкою розширень, у тому числі Шаблон:Не перекладено та екзистенційних типівШаблон:Sfn.

Спеціальні змінні типу

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

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

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

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

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

Література

• Шаблон:Стаття
• Шаблон:Стаття

Посилання

• Шаблон:Cite web
• Шаблон:Cite web
• Шаблон:Cite web
• Шаблон:Cite web
• Шаблон:Стаття