Система F

Систе́ма F (полімо́рфне ля́мбда-чи́слення, систе́ма $\lambda 2$, типізо́ване ля́мбда-чи́слення дру́гого поря́дку) — система типізованого лямбда-числення, що відрізняється від просто типізованої системи наявністю механізму універсальної квантифікації над типами. Цю систему розробив 1972 року Шаблон:Нп у контексті теорії доведень у логіці. Незалежно від нього подібну систему запропонував 1974 року Шаблон:Нп. Система F дозволяє формалізувати концепцію параметричного поліморфізму в мовах програмування та слугує теоретичною основою для таких мов програмування як Haskell та ML.

Система F допускає конструювання термів, залежних від типів. Технічно це досягається через механізм абстрагування терму за типом, що в результаті дає новий терм. Традиційно для такої абстракції використовують символ великої лямбди $\mathrm{\Lambda }$. Наприклад, взявши терм $\lambda x^{\alpha }.x$ типу $\alpha \to \alpha$ та абстрагуючись за змінною типу $\alpha$, отримуємо терм $\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.x$. Цей терм є функцією з типів у терми. Застосовуючи цю функцію до різних типів, ми отримуватимемо терми з ідентичною структурою, але різними типами:

$(\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.x)\mathtt{\text{Bool}}{\to }_{\beta }\lambda x^{\mathtt{\text{Bool}}}.x$ — терм типу $\mathtt{\text{Bool}}\to \mathtt{\text{Bool}}$;

$(\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.x)\mathtt{\text{Nat}}{\to }_{\beta }\lambda x^{\mathtt{\text{Nat}}}.x$ — терм типу $\mathtt{\text{Nat}}\to \mathtt{\text{Nat}}$.

Видно, що терм $\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.x$ має поліморфну поведінку, тобто задає спільний інтерфейс для різних типів даних. У системі F цьому терму приписується тип $\mathrm{\forall }\alpha .\alpha \to \alpha$. Квантор загальності в типі підкреслює можливість підстановки замість змінної типу $\alpha$ будь-якого допустимого типу.

Формальний опис

Синтаксис типів

Типи Системи F конструюються із набору змінних типу за допомогою операторів $\to$ і $\mathrm{\forall }$ . За традицією для змінних типу використовують грецькі літери. Правила формування типів такі:

• (Змінна типу) Якщо $\alpha$ — змінна типу, то $\alpha$ — це тип;
• (Стрілковий тип) Якщо $A$ і $B$ є типами, то $(A\to B)$ — це тип;
• (Універсальний тип) Якщо $\alpha$ є змінною типу, а $B$ — типом, то $(\mathrm{\forall }\alpha .B)$ — це тип.

Зовнішні дужки часто опускають, оператор $\to$ вважають правоасоціативним, а дію оператора $\mathrm{\forall }$ такою, що продовжується праворуч наскільки це можливо. Наприклад, $\mathrm{\forall }\alpha .\mathrm{\forall }\beta .\alpha \to \beta \to \alpha$ — стандартне скорочення для $(\mathrm{\forall }\alpha .(\mathrm{\forall }\beta .(\alpha \to (\beta \to \alpha ))))$.

Синтаксис термів

Терми системи F конструюються з набору термових змінних ($x$, $y$, $z$ і т. д.) за такими правилами

• (Змінна) Якщо $x$ — змінна, то $x$ — це терм;
• (Абстракція) Якщо $x$ є змінною, $A$ — типом, а $M$ — термом, то $(\lambda x^A.M)$ — це терм;
• (Застосування) Якщо $M$ і $N$ є термами, то $(MN)$ — це терм;
• (Універсальна абстракція) Якщо $\alpha$ є змінною типу, а $M$ — термом, то $(\mathrm{\Lambda }\alpha .M)$ — це терм;
• (Універсальне застосування) Якщо $M$ є термом, а $A$ — типом, то $(MA)$ — це терм.

Зовнішні дужки часто опускають, обидва сорти застосування вважають лівоасоціативними, а дію абстракцій — такою, що продовжується вправо наскільки це можливо.

Розрізняють дві версії просто типізованої системи. Якщо, як у наведених вище правилах, термові змінні в лямбда-абстракції анотуються типами, то систему називають типізованою за Чорчем. Якщо ж правило абстракції замінити на

• (Абстракція за Каррі) Якщо $x$ є змінною, а $M$ — термом, то $(\lambda x.M)$ — це терм, і відкинути два останні правила, то систему називають типізованою за Каррі. Фактично, терми системи, типізованої за Каррі, ті самі, що й у безтиповому лямбда-численні.

Правила редукції

Крім стандартного для лямбда-обчислення правила $\beta$ -редукції

$(\lambda a^A.M)N{\to }_{\beta }M[a:=N]$

у системі F у стилі Чорча вводиться додаткове правило,

$(\mathrm{\Lambda }\alpha .M)A{\to }_{\beta }M[\alpha :=A]$,

що дозволяє обчислювати застосування терму до типу через механізм підстановки типу замість змінної типу.

Контексти типізації та затвердження типізації

Контекстом, як і в просто типізованому лямбда-обчисленні, називають множину тверджень про приписування типів різним змінним, розділених комою

$\mathrm{\Gamma }=x_1:A_1,x_2:A_1,\dots ,x_n:A_n$

У контекст можна додати «свіжу» для цього контексту змінну: якщо $\mathrm{\Gamma }$ — допустимий контекст, який не містить змінної $x$, а $B$ — тип, то $\mathrm{\Gamma },x:B$ — теж допустимий контекст.

Загальний вигляд твердження про типізацію такий:

$\mathrm{\Gamma }⊢M:A$

Це читається так: у контексті $\mathrm{\Gamma }$ терм $M$ має тип $A$.

Правила типізації за Чорчем

У системі F, типізованій за Чорчем, типи термам приписують за такими правилами: (Початкове правило) Якщо змінна $x$ пирсутня в контексті $\mathrm{\Gamma }$ з типом $A$, то в цьому контексті $x$ має тип $A$. У вигляді правила виведення

$\frac{x:A\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:A}$

(Правило введення $\to$) Якщо в деякому контексті, розширеному твердженням, що $a$ має тип $A$, терм $M$ має тип $B$, то в згаданому контексті (без $a$), лямбда-абстракція $\lambda a^A.M$ має тип $A\to B$. У вигляді правила виведення

$\frac{\mathrm{\Gamma },a:A⊢M:B}{\mathrm{\Gamma }⊢(\lambda a^A.M):(A\to B)}$

(Правило видалення $\to$) Якщо в деякому контексті терм $M$ має тип $A\to B$, а терм $N$ має тип $A$, то застосування $MN$ має тип $B$ . У вигляді правила виведення

$\frac{\mathrm{\Gamma }⊢M:(A\to B)\mathrm{\Gamma }⊢N:A}{\mathrm{\Gamma }⊢(MN):B}$

(Правило введення $\mathrm{\forall }$) Якщо в деякому контексті терм $M$ має тип $A$, то в цьому контексті терм $\mathrm{\Lambda }\alpha .M$ має тип $\mathrm{\forall }\alpha .A$. У вигляді правила виведення

$\frac{\mathrm{\Gamma }⊢M:A}{\mathrm{\Gamma }⊢(\mathrm{\Lambda }\alpha .M):(\mathrm{\forall }\alpha .A)}$

Це правило вимагає застереження: змінна типу $\alpha$ не повинна зустрічатися у твердженнях типізації контексту $\mathrm{\Gamma }$.

(Правило видалення $\mathrm{\forall }$) Якщо в деякому контексті терм $M$ має тип $\mathrm{\forall }\alpha .A$, і $B$ — це тип, то в цьому контексті терм $MB$ має тип $A[\alpha :=B]$. У вигляді правила виведення

$\frac{\mathrm{\Gamma }⊢M:(\mathrm{\forall }\alpha .A)}{\mathrm{\Gamma }⊢(MB):(A[\alpha :=B])}$

Правила типізації за Каррі

У системі F, типізованій за Каррі, приписування типів терм здійснюється відповідно до таких правил: (Початкове правило) Якщо змінна $x$ в контексті $\mathrm{\Gamma }$ присутня з типом $A$, то в цьому контексті $x$ має тип $A$. У вигляді правила виведення

$\frac{x:A\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:A}$

(Правило введення $\to$) Якщо в деякому контексті, розширеному твердженням, що $a$ має тип $A$, терм $M$ має тип $B$, то в згаданому контексті (без $a$), лямбда-абстракція $\lambda a.M$ має тип $A\to B$ . У вигляді правила виведення

$\frac{\mathrm{\Gamma },a:A⊢M:B}{\mathrm{\Gamma }⊢(\lambda a.M):(A\to B)}$

(Правило видалення $\to$) Якщо в деякому контексті терм $M$ має тип $A\to B$, а терм $N$ має тип $A$, то застосування $MN$ має тип $B$. У вигляді правила виведення

$\frac{\mathrm{\Gamma }⊢M:(A\to B)\mathrm{\Gamma }⊢N:A}{\mathrm{\Gamma }⊢(MN):B}$

(Правило введення $\mathrm{\forall }$) Якщо в деякому контексті терм $M$ має тип $A$, то в цьому контексті цьому терму $M$ можна приписати і тип $\mathrm{\forall }\alpha .A$ . У вигляді правила виведення

$\frac{\mathrm{\Gamma }⊢M:A}{\mathrm{\Gamma }⊢M:(\mathrm{\forall }\alpha .A)}$

Це правило вимагає застереження: змінна типу $\alpha$ не повинна зустрічатися у твердженнях типізації контексту $\mathrm{\Gamma }$.

(Правило видалення $\mathrm{\forall }$) Якщо в деякому контексті терм $M$ має тип $\mathrm{\forall }\alpha .A$, і $B$ — це тип, то в цьому контексті цьому терму $M$ можна приписати й тип $A[\alpha :=B]$. У вигляді правила виведення

$\frac{\mathrm{\Gamma }⊢M:(\mathrm{\forall }\alpha .A)}{\mathrm{\Gamma }⊢M:(A[\alpha :=B])}$

Приклад

За початковим правилом:

$x:(\mathrm{\forall }\alpha .\alpha \to \alpha )⊢x:(\mathrm{\forall }\alpha .\alpha \to \alpha )$

Застосуємо правило видалення $\mathrm{\forall }$, взявши як $B$ тип $\mathrm{\forall }\alpha .\alpha \to \alpha$

$x:(\mathrm{\forall }\alpha .\alpha \to \alpha )⊢x:(\mathrm{\forall }\alpha .\alpha \to \alpha )\to (\mathrm{\forall }\alpha .\alpha \to \alpha )$

Тепер за правилом видалення $\to$ маємо можливість застосувати терм $x$ сам до себе

$x:(\mathrm{\forall }\alpha .\alpha \to \alpha )⊢(xx):(\mathrm{\forall }\alpha .\alpha \to \alpha )$

і, нарешті, за правилом введення $\to$

$⊢(\lambda x.xx):(\mathrm{\forall }\alpha .\alpha \to \alpha )\to (\mathrm{\forall }\alpha .\alpha \to \alpha )$

Це приклад терму, що типізується в системі F, але не в просто типізованій системі .

Подання типів даних

Система F має достатні виражальні засоби, для того щоб безпосередньо реалізувати багато типів даних, що використовуються в мовах програмування. Працюватимемо у версії Чорча системи F.

Порожній тип. Тип

$\mathrm{\perp }\equiv \mathrm{\forall }\alpha .\alpha$

ненаселений у системі F, тобто у ній відсутні терми з таким типом.

Одиничний тип. У типу

$\mathrm{\top }\equiv \mathrm{\forall }\alpha .\alpha \to \alpha$

в системі F є єдиний мешканець, що перебуває в нормальній формі, — терм.

$𝚒𝚍\equiv \mathrm{\Lambda }\alpha .\lambda x^{\alpha }.x$.

Булів тип. У системі F задається так:

$𝙱𝚘𝚘𝚕\equiv \mathrm{\forall }\alpha .\alpha \to \alpha \to \alpha$.

У цього типу рівно два мешканці, ототожнювані з двома булевими константами.

$𝚝𝚛𝚞𝚎\equiv \mathrm{\Lambda }\alpha .\lambda x^{\alpha }.\lambda y^{\alpha }.x$

$𝚏𝚊𝚕𝚜𝚎\equiv \mathrm{\Lambda }\alpha .\lambda x^{\alpha }.\lambda y^{\alpha }.y$

Конструкція умовного оператора

$𝚒𝚏𝚃𝚑𝚎𝚗𝙴𝚕𝚜𝚎\equiv \mathrm{\Lambda }\alpha .\lambda b^{𝙱𝚘𝚘𝚕}.\lambda x^{\alpha }.\lambda y^{\alpha }.b\alpha xy$

Ця функція відповідає природним вимогам

$𝚒𝚏𝚃𝚑𝚎𝚗𝙴𝚕𝚜𝚎A𝚝𝚛𝚞𝚎MN=M$

і

$𝚒𝚏𝚃𝚑𝚎𝚗𝙴𝚕𝚜𝚎A𝚏𝚊𝚕𝚜𝚎MN=N$

для довільного типу $A$ та довільних $M:A$ і $N:A$. У цьому легко переконатися, розкривши визначення та виконавши $\beta$ -редукції.

Тип добутку. Для довільних типів $A$ і $B$ тип їх декартового твору

$A\times B\equiv \mathrm{\forall }\alpha .(A\to B\to \alpha )\to \alpha$

населений парою

$⟨M;N⟩\equiv \mathrm{\Lambda }\alpha .\lambda f^{(A\to B\to \alpha )}.fMN$

для кожних $M:A$ і $N:B$. Проєкції пари задаються функціями

$𝚏𝚜𝚝\equiv \mathrm{\Lambda }\alpha .\mathrm{\Lambda }\beta .\lambda p^{\alpha \times \beta }.p\alpha (\lambda x^{\alpha }.\lambda y^{\beta }.x):\mathrm{\forall }\alpha .\mathrm{\forall }\beta .\alpha \times \beta \to \alpha$

$𝚜𝚗𝚍\equiv \mathrm{\Lambda }\alpha .\mathrm{\Lambda }\beta .\lambda p^{\alpha \times \beta }.p\beta (\lambda x^{\alpha }.\lambda y^{\beta }.y):\mathrm{\forall }\alpha .\mathrm{\forall }\beta .\alpha \times \beta \to \beta$

Ці функції відповідають природним вимогам $𝚏𝚜𝚝AB⟨M;N⟩=M$ і $𝚜𝚗𝚍AB⟨M;N⟩=N$ .

Тип суми. Для довільних типів $A$ і $B$ тип їх суми

$A+B\equiv \mathrm{\forall }\alpha .(A\to \alpha )\to (B\to \alpha )\to \alpha$

населений або термом типу $A$, або термом типу $B$, залежно від застосованого конструктора

$𝚒𝚗𝚓𝙻M\equiv \mathrm{\Lambda }\alpha .\lambda f^{A\to \alpha }.\lambda g^{B\to \alpha }.fM$

$𝚒𝚗𝚓𝚁N\equiv \mathrm{\Lambda }\alpha .\lambda f^{A\to \alpha }.\lambda g^{B\to \alpha }.gN$

Тут $M:A$, $N:B$. Функція, що здійснює розбір випадків (порівняння зі взірцем), має вигляд

$𝚖𝚊𝚝𝚌𝚑\equiv \mathrm{\Lambda }\alpha .\mathrm{\Lambda }\beta .\mathrm{\Lambda }\gamma .\lambda s^{\alpha +\beta }.\lambda f^{\alpha \to \gamma }.\lambda g^{\beta \to \gamma }.s\gamma fg:\mathrm{\forall }\alpha .\mathrm{\forall }\beta .\mathrm{\forall }\gamma .\alpha +\beta \to (\alpha \to \gamma )\to (\beta \to \gamma )\to \gamma$

Ця функція відповідає таким природним вимогам

$𝚖𝚊𝚝𝚌𝚑ABC(𝚒𝚗𝚓𝙻M)FG=FM$

і

$𝚖𝚊𝚝𝚌𝚑ABC(𝚒𝚗𝚓𝚁N)FG=GN$

для довільних типів $A$, $B$ і $C$ та довільних термів $F:A\to C$ і $G:B\to C$.

Числа Чорча. Тип натуральних чисел у системі F

$𝙽𝚊𝚝\equiv \mathrm{\forall }\alpha .\alpha \to (\alpha \to \alpha )\to \alpha$

населений нескінченною кількістю різних елементів, одержуваних за допомогою двох конструкторів $𝚣𝚎𝚛𝚘:𝙽𝚊𝚝$ і $𝚜𝚞𝚌𝚌:𝙽𝚊𝚝\to 𝙽𝚊𝚝$:

$𝚣𝚎𝚛𝚘\equiv \mathrm{\Lambda }\alpha .\lambda z^{\alpha }.\lambda s^{\alpha \to \alpha }.z$

$𝚜𝚞𝚌𝚌\equiv \lambda n^{𝙽𝚊𝚝}.\mathrm{\Lambda }\alpha .\lambda z^{\alpha }.\lambda s^{\alpha \to \alpha }.s(n\alpha zs)$

Натуральне число $n$ можна отримати застосувавши $n$ разів другий конструктор до першого або, еквівалентно, подати термом

$\bar{n}\equiv \mathrm{\Lambda }\alpha .\lambda z^{\alpha }.\lambda s^{\alpha \to \alpha }.\underset{n}{\underbrace{s(s(s\dots (s}}z)\dots ))$

Властивості

• Просто типізована система має властивість ти́пової безпеки: при $\beta$-редукціях тип лямбда-терму залишається незмінним, а сама типізація не заважає перебігу обчислень.

• У своїй дисертації Шаблон:Нп показав, що система F має властивість сильної нормалізації: будь-який допустимий терм за скінченне число $\beta$-редукцій зводиться до єдиної нормальної форми.

• Система F є імпредикативною системою, оскільки змінна типу, що зв'язується квантором загальності при визначенні універсального типу, може заміщатися самим об'єктом, що визначається. Наприклад, терм $\mathtt{\text{id}}$ одиничного типу $\mathrm{\top }\equiv \mathrm{\forall }\alpha .\alpha \to \alpha$ можна застосувати до власного типу, породжуючи терм типу $\mathrm{\top }\to \mathrm{\top }$. Як показав Джо Веллз (Joe Wells) 1994 року, задача виведення типів для версії Каррі системи F нерозв'язна. Тому при практичній реалізації мов програмування зазвичай використовують обмежені, предикативні версії поліморфізму: пренекс-поліморфізм (поліморфізм у стилі ML), поліморфізм рангу 2 тощо. У разі пренекс-поліморфізму областю визначення змінних типу є лише типи без кванторів. У цих системах задачу виведення типів можна розв'язати, такий висновок базується на алгоритмі Гіндлі — Мілнера.

• Відповідність Каррі — Говарда пов'язує систему F із мінімальною інтуїціоністською Шаблон:Iw, формули якої побудовано з пропозиційних змінних за допомогою імплікації та універсальної квантифікації за висловлюваннями. При цьому значення $\mathrm{\top }$ (істина), $\mathrm{\perp }$ (брехня), зв'язки $\mathrm{\neg }$ (заперечення), $\wedge$ (кон'юнкція) та $\vee$ (диз'юнкція), а також $\mathrm{\exists }$ (квантор існування) можна визначити так

$\mathrm{\top }\equiv \mathrm{\forall }\alpha .\alpha \to \alpha$

$\mathrm{\perp }\equiv \mathrm{\forall }\alpha .\alpha$

$\mathrm{\neg }A\equiv A\to \mathrm{\perp }$

$A\wedge B\equiv \mathrm{\forall }\alpha .(A\to B\to \alpha )\to \alpha$

$A\vee B\equiv \mathrm{\forall }\alpha .(A\to \alpha )\to (B\to \alpha )\to \alpha$

$\mathrm{\exists }\alpha .M[\alpha ]\equiv \mathrm{\forall }\gamma .(\mathrm{\forall }\alpha .M[\alpha ]\to \gamma )\to \gamma$

Зазначимо, що відповідність Каррі — Говарда ставить у відповідність до істини — одиничний тип, брехні — порожній тип, кон'юнкції — добуток типів, а диз'юнкції — їх суму.

Література

• Шаблон:Книга
• Шаблон:Стаття
• Шаблон:Книга