Система F

Систе́ма F (полімо́рфне ля́мбда-чи́слення, систе́ма ${\displaystyle \lambda 2}$, типізо́ване ля́мбда-чи́слення дру́гого поря́дку) — система типізованого лямбда-числення, що відрізняється від просто типізованої системи наявністю механізму універсальної квантифікації над типами. Цю систему розробив 1972 року Жан-Ів Жирар^[en][1] у контексті теорії доведень у логіці. Незалежно від нього подібну систему запропонував 1974 року Джон Рейнольдс^[en][2]. Система F дозволяє формалізувати концепцію параметричного поліморфізму в мовах програмування та слугує теоретичною основою для таких мов програмування як Haskell та ML.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle \Gamma =x_{1}\!:\!A_{1},x_{2}\!:\!A_{1},\ldots ,x_{n}\!:\!A_{n}}$

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

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

${\displaystyle \Gamma \vdash M\!:\!A}$

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

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

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

${\displaystyle {x\!:\!A\in \Gamma } \over {\Gamma \vdash x\!:\!A}}$

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

${\displaystyle {\Gamma ,a\!:\!A\vdash M\!:\!B} \over {\Gamma \vdash (\lambda a^{A}.~M)\!:\!(A\to B)}}$

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

${\displaystyle {\Gamma \vdash M\!:\!(A\to B)\quad \Gamma \vdash N\!:\!A} \over {\Gamma \vdash (M~N)\!:\!B}}$

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

${\displaystyle {\Gamma \vdash M\!:\!A} \over {\Gamma \vdash (\Lambda \alpha .~M)\!:\!(\forall \alpha .~A)}}$

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

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

${\displaystyle {\Gamma \vdash M\!:\!(\forall \alpha .~A)} \over {\Gamma \vdash (M~B)\!:\!(A[\alpha :=B])}}$

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

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

${\displaystyle {x\!:\!A\in \Gamma } \over {\Gamma \vdash x\!:\!A}}$

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

${\displaystyle {\Gamma ,a\!:\!A\vdash M\!:\!B} \over {\Gamma \vdash (\lambda a.~M)\!:\!(A\to B)}}$

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

${\displaystyle {\Gamma \vdash M\!:\!(A\to B)\quad \Gamma \vdash N\!:\!A} \over {\Gamma \vdash (M~N)\!:\!B}}$

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

${\displaystyle {\Gamma \vdash M\!:\!A} \over {\Gamma \vdash M\!:\!(\forall \alpha .~A)}}$

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

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

${\displaystyle {\Gamma \vdash M\!:\!(\forall \alpha .~A)} \over {\Gamma \vdash M\!:\!(A[\alpha :=B])}}$

Приклад

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

${\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )}$

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

${\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )}$

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

${\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash (x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )}$

і, нарешті, за правилом введення ${\displaystyle \rightarrow }$

${\displaystyle \vdash (\lambda x.~x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )}$

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

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

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

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

${\displaystyle \bot \ \equiv \ \forall \alpha .~\alpha }$

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

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

${\displaystyle \top \ \equiv \ \forall \alpha .~\alpha \to \alpha }$

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

${\displaystyle {\mathtt {id}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~x}$.

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

${\displaystyle {\mathtt {Bool}}\ \equiv \ \forall \alpha .~\alpha \to \alpha \to \alpha }$.

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

${\displaystyle {\mathtt {true}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~x}$

${\displaystyle {\mathtt {false}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~y}$

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

${\displaystyle {\mathtt {ifThenElse}}\ \equiv \ \Lambda \alpha .~\lambda b^{\mathtt {Bool}}.~\lambda x^{\alpha }.~\lambda y^{\alpha }.~b\,\alpha \,x\,y}$

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

${\displaystyle {\mathtt {ifThenElse}}\,A\,{\mathtt {true}}\,M\,N=M}$

і

${\displaystyle {\mathtt {ifThenElse}}\,A\,{\mathtt {false}}\,M\,N=N}$

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

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

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

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

${\displaystyle \langle M;N\rangle ~\equiv ~\Lambda \alpha .~\lambda f^{(A\to B\to \alpha )}.~f~M~N}$

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

${\displaystyle {\mathtt {fst}}\ \equiv \ \Lambda \alpha .~\Lambda \beta .~\lambda p^{\alpha \times \beta }.~p\,\alpha \,(\lambda x^{\alpha }.\,\lambda y^{\beta }.\,x)~:~\forall \alpha .~\forall \beta .\,\alpha \times \beta \to \alpha }$

${\displaystyle {\mathtt {snd}}\ \equiv \ \Lambda \alpha .~\Lambda \beta .~\lambda p^{\alpha \times \beta }.~p\,\beta \,(\lambda x^{\alpha }.\,\lambda y^{\beta }.\,y)~:~\forall \alpha .~\forall \beta .\,\alpha \times \beta \to \beta }$

Ці функції відповідають природним вимогам ${\displaystyle {\mathtt {fst}}\,A\,B\,\langle M;N\rangle =M}$ і ${\displaystyle {\mathtt {snd}}\,A\,B\,\langle M;N\rangle =N}$ .

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

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

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

${\displaystyle {\mathtt {injL}}\,M~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }.\,f\,M}$

${\displaystyle {\mathtt {injR}}\,N~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }.\,g\,N}$

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

${\displaystyle {\mathtt {match}}~\equiv ~\Lambda \alpha .\,\Lambda \beta .\,\Lambda \gamma .\,\lambda s^{\alpha +\beta }.\,\lambda f^{\alpha \to \gamma }.\,\lambda g^{\beta \to \gamma }.\,s\,\gamma \,f\,g~:~\forall \alpha .~\forall \beta .~\forall \gamma .~\alpha +\beta \to (\alpha \to \gamma )\to (\beta \to \gamma )\to \gamma }$

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

${\displaystyle {\mathtt {match}}\,A\,B\,C\,({\mathtt {injL}}\,M)\,F\,G=F\,M}$

і

${\displaystyle {\mathtt {match}}\,A\,B\,C\,({\mathtt {injR}}\,N)\,F\,G=G\,N}$

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

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

${\displaystyle {\mathtt {Nat}}\ \equiv \ \forall \alpha .~\alpha \to (\alpha \to \alpha )\to \alpha }$

населений нескінченною кількістю різних елементів, одержуваних за допомогою двох конструкторів ${\displaystyle {\mathtt {zero}}\!:\!{\mathtt {Nat}}}$ і ${\displaystyle {\mathtt {succ}}\!:\!{\mathtt {Nat}}\to {\mathtt {Nat}}}$:

${\displaystyle {\mathtt {zero}}\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,z}$

${\displaystyle {\mathtt {succ}}\ \equiv \ \lambda n^{\mathtt {Nat}}.\,\Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,s\,(n\,\alpha \,z\,s)}$

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

${\displaystyle {\overline {n}}\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \rightarrow \alpha }.\,\underbrace {s(s(s\ldots (s} _{n}\,z)\ldots ))}$

Властивості

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

• У своїй дисертації Жан-Ів Жирар^[en] показав^[1], що система F має властивість сильної нормалізації: будь-який допустимий терм за скінченне число ${\displaystyle \beta }$-редукцій зводиться до єдиної нормальної форми.

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

• Відповідність Каррі — Говарда пов'язує систему F із мінімальною інтуїціоністською логікою висловлювань другого порядку^[en], формули якої побудовано з пропозиційних змінних за допомогою імплікації та універсальної квантифікації за висловлюваннями. При цьому значення ${\displaystyle \top }$ (істина), ${\displaystyle \bot }$ (брехня), зв'язки ${\displaystyle \lnot }$ (заперечення), ${\displaystyle \land }$ (кон'юнкція) та ${\displaystyle \lor }$ (диз'юнкція), а також ${\displaystyle \exists }$ (квантор існування) можна визначити так

${\displaystyle \top ~\equiv ~\forall \alpha .\,\alpha \to \alpha }$

${\displaystyle \bot ~\equiv ~\forall \alpha .\,\alpha }$

${\displaystyle \lnot A~\equiv ~A\to \bot }$

${\displaystyle A\land B~\equiv ~\forall \alpha .\,(A\to B\to \alpha )\to \alpha }$

${\displaystyle A\lor B~\equiv ~\forall \alpha .\,(A\to \alpha )\to (B\to \alpha )\to \alpha }$

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

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

Примітки

1. Girard, Jean-Yves. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. — Université Paris 7, 1972.
2. John C. Reynolds. Towards a Theory of Type Structure : [арх. 31 жовтня 2014]. — 1974.
3. Wells J. B. Typability and type checking in the second-order lambda-calculus are equivalent and undecidable : [арх. 22 лютого 2007] // Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). — 1994. — С. 176–185.

Література

• Pierce, Benjamin C. Types and Programming Languages. — MIT Press, 2002. — ISBN 0-262-16209-1.
• Barendregt, Henk. Lambda Calculi with Types // Handbook of Logic in Computer Science. — Oxford University Press, 1992. — Т. II (4 листопада). — С. 117-309.
• Jean-Yves Girard, Paul Taylor, Yves Lafont. Proofs and Types. — Cambridge University Press, 1989. — ISBN 0 521 37181 3.