Змінна типу

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

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

Приклад

У такому визначенні «список» мовою Standard ML, ідентифікатор 'a (читається «альфа») є змінною типу:

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

При використанні цього у типову змінну підставляється конкретний тип, так що в програмі можна сформувати багато мономорфних типів: string list, int list, int list list і т. д. За такої підстановки замість кожної згадки змінної типу підставляється один і той самий тип. Отримана інформація про типи використовується для верифікації та оптимізації програми, після чого зазвичай стирається, тому один і той самий цільовий код обробляє об'єкти спочатку різних типів (але існують і винятки з цього правила, зокрема, в ). Якщо поліморфний тип параметризовано декількома змінними типу, то типи можуть бути як різними, так і ідентичними, але правило підстановки дотримується. Наприклад, якщо такий тип:

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}$. Такий запис називають ^[en]. Велика ${\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 з та низкою розширень, у тому числі ^[en] та екзистенційних типів.

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

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

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

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

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

Слабкі змінні типу (weak type variables) використовувалися в компіляторі ^[en] як альтернатива імперативним змінним типу, надаючи істотно більші можливості (точніше, менші обмеження). Позначаються '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. — 17 липня.
11. Andrew W. Appel. A Critique of Standard ML. — Princeton University, revised version of CS-TR-364-92, 1992. — 17 липня.

Література

• 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.