Система F

Система F (полиморфное лямбда-исчисление, система $\lambda 2$ , типизированное лямбда-исчисление второго порядка) — система типизированного лямбда-исчисления, отличающаяся от просто типизированной системы наличием механизма универсальной квантификации над типами. Эту систему разработал в 1972 году Жан-Ив Жирар [1] в контексте теории доказательств в логике. Независимо от него подобную систему предложил в 1974 году Джон Рейнольдс[2]. Система F позволяет формализовать концепцию параметрического полиморфизма в языках программирования и служит теоретической основой для таких языков программирования как Haskell и ML.

Система F допускает конструирование термов, зависящих от типов. Технически это достигается через механизм абстрагирования терма по типу, что в результате даёт новый терм. Традиционно для такой абстракции используют символ большой лямбды $\Lambda$ . Например, взяв терм $\lambda x^{\alpha }.~x$ типа $\alpha \to \alpha$ и абстрагируясь по переменной типа $\alpha$ , получаем терм $\Lambda \alpha .~\lambda x^{\alpha }.~x$ . Этот терм представляет собой функцию из типов в термы. Применяя эту функцию к различным типам, мы будем получать термы с идентичной структурой, но разными типами:

(\Lambda \alpha .~\lambda x^{\alpha }.~x)~{\texttt {Bool}}\ \to _{\beta }\ \lambda x^{\texttt {Bool}}.~x

— терм типа

{\texttt {Bool}}\to {\texttt {Bool}}

;

(\Lambda \alpha .~\lambda x^{\alpha }.~x)~{\texttt {Nat}}\ \to _{\beta }\ \lambda x^{\texttt {Nat}}.~x

— терм типа

{\texttt {Nat}}\to {\texttt {Nat}}

.

Видно, что терм $\Lambda \alpha .~\lambda x^{\alpha }.~x$ обладает полиморфным поведением, то есть задаёт общий интерфейс для различных типов данных. В Системе F этому терму приписывается тип $\forall \alpha .~\alpha \to \alpha$ . Квантор всеобщности в типе подчёркивает возможность подстановки вместо переменной типа $\alpha$ любого допустимого типа.

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

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

Типы Системы F конструируются из набора переменных типа с помощью операторов $\to$ и $\forall$ . По традиции для переменных типа используют греческие буквы. Правила формирования типов таковы:

(Переменная типа) Если $\alpha$ — переменная типа, то $\alpha$ — это тип;
(Стрелочный тип) Если $A$ и $B$ являются типами, то $(A\to B)$ — это тип;
(Универсальный тип) Если $\alpha$ является переменной типа, а $B$ — типом, то $(\forall \alpha .~B)$ — это тип.

Внешние скобки часто опускают, оператор $\rightarrow$ считают правоассоциативным, а действие оператора $\forall$ продолжающимся вправо насколько это возможно. Например, $\forall \alpha .~\forall \beta .~\alpha \to \beta \to \alpha$ — стандартное сокращение для $(\forall \alpha .~(\forall \beta .~(\alpha \to (\beta \to \alpha ))))$ .

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

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

(Переменная) Если $x$ — переменная, то $x$ — это терм;
(Абстракция) Если $x$ является переменной, $A$ — типом, а $M$ — термом, то $(\lambda x^{A}.~M)$ — это терм;
(Применение) Если $M$ и $N$ являются термами, то $(M~N)$ — это терм;
(Универсальная абстракция) Если $\alpha$ является переменной типа, а $M$ — термом, то $(\Lambda \alpha .~M)$ — это терм;
(Универсальное применение) Если $M$ является термом, а $A$ — типом, то $(M~A)$ — это терм.

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

Различают две версии просто типизированной системы. Если, как в приведённых выше правилах, термовые переменные в лямбда-абстракции аннотируются типами, то систему называют типизированной по Чёрчу. Если же правило абстракции заменить на

(Абстракция по Карри) Если $x$ является переменной, а $M$ — термом, то $(\lambda x.~M)$ — это терм,

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

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

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

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

в системе F в стиле Чёрча вводится дополнительное правило,

{\displaystyle (\Lambda \alpha .~M)~A\ \to _{\beta }\ M[\alpha

,

позволяющее вычислять применение терма к типу через механизм подстановки типа вместо переменной типа.

Контексты типизации и утверждение типизации

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

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

В контекст можно добавить «свежую» для этого контекста переменную: если $\Gamma$ — допустимый контекст, не содержащий переменной $x$ , а $B$ — тип, то $\Gamma ,x\!:\!B$ — тоже допустимый контекст.

Общий вид утверждения о типизации таков:

\Gamma \vdash M\!:\!A

Это читается следующим образом: в контексте $\Gamma$ терм $M$ имеет тип $A$ .

Правила типизации по Чёрчу

В Системе F, типизированной по Чёрчу, приписывание типов термам осуществляется в соответствии со следующими правилами:

(Начальное правило) Если переменная $x$ присутствует с типом $A$ в контексте $\Gamma$ , то в этом контексте $x$ имеет тип $A$ . В виде правила вывода

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

(Правило введения $\rightarrow$ ) Если в некотором контексте, расширенном утверждением, что $a$ имеет тип $A$ , терм $M$ имеет тип $B$ , то в упомянутом контексте (без $a$ ), лямбда-абстракция $\lambda a^{A}.~M$ имеет тип $A\to B$ . В виде правила вывода

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

(Правило удаления $\rightarrow$ ) Если в некотором контексте терм $M$ имеет тип $A\to B$ , а терм $N$ имеет тип $A$ , то применение $M~N$ имеет тип $B$ . В виде правила вывода

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

(Правило введения $\forall$ ) Если в некотором контексте терм $M$ имеет тип $A$ , то в этом контексте терм $\Lambda \alpha .~M$ имеет тип $\forall \alpha .~A$ . В виде правила вывода

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

Это правило требует оговорки: переменная типа $\alpha$ не должна встречаться в утверждениях типизации контекста $\Gamma$ .

(Правило удаления $\forall$ ) Если в некотором контексте терм $M$ имеет тип $\forall \alpha .~A$ , и $B$ — это тип, то в этом контексте терм $M~B$ имеет тип ${\displaystyle A[\alpha$ . В виде правила вывода

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

Правила типизации по Карри

В Системе F, типизированной по Карри, приписывание типов термам осуществляется в соответствии со следующими правилами:

(Начальное правило) Если переменная $x$ присутствует с типом $A$ в контексте $\Gamma$ , то в этом контексте $x$ имеет тип $A$ . В виде правила вывода

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

(Правило введения $\rightarrow$ ) Если в некотором контексте, расширенном утверждением, что $a$ имеет тип $A$ , терм $M$ имеет тип $B$ , то в упомянутом контексте (без $a$ ), лямбда-абстракция $\lambda a.~M$ имеет тип $A\to B$ . В виде правила вывода

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

(Правило удаления $\rightarrow$ ) Если в некотором контексте терм $M$ имеет тип $A\to B$ , а терм $N$ имеет тип $A$ , то применение $M~N$ имеет тип $B$ . В виде правила вывода

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

(Правило введения $\forall$ ) Если в некотором контексте терм $M$ имеет тип $A$ , то в этом контексте этому терму $M$ может быть приписан и тип $\forall \alpha .~A$ . В виде правила вывода

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

Это правило требует оговорки: переменная типа $\alpha$ не должна встречаться в утверждениях типизации контекста $\Gamma$ .

(Правило удаления $\forall$ ) Если в некотором контексте терм $M$ имеет тип $\forall \alpha .~A$ , и $B$ — это тип, то в этом контексте этому терму $M$ может быть приписан и тип ${\displaystyle A[\alpha$ . В виде правила вывода

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

Пример. По начальному правилу:

x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )

Применим правило удаления $\forall$ , взяв в качестве $B$ тип $\forall \alpha .~\alpha \to \alpha$

x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )

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

x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash (x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )

и, наконец, по правилу введения $\rightarrow$

\vdash (\lambda x.~x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )

Это пример терма, типизируемого в Системе F, но не в просто типизированной системе.

Представление типов данных

Система F обладает достаточными выразительными средствами, для того чтобы напрямую реализовать многие типы данных, используемые в языках программирования. Будем работать в версии Чёрча системы F.

Пустой тип. Тип

\bot \ \equiv \ \forall \alpha .~\alpha

необитаем в системе F, то есть в ней отсутствуют термы с таким типом.

Единичный тип. У типа

\top \ \equiv \ \forall \alpha .~\alpha \to \alpha

в системе F имеется единственный находящийся в нормальной форме обитатель — терм

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

.

Булев тип. В системе F задается так:

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

.

У этого типа ровно два обитателя, отождествляемых с двумя булевыми константами

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

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

Конструкция условного оператора

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

Эта функция удовлетворяет естественным требованиям

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

и

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

для произвольного типа $A$ и произвольных $M\!:\!A$ и $N\!:\!A$ . В этом легко убедиться, раскрыв определения и выполнив $\beta$ -редукции.

Тип произведения. Для произвольных типов $A$ и $B$ тип их декартова произведения

A\times B~\equiv ~\forall \alpha .~(A\to B\to \alpha )\to \alpha

населён парой

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

для каждых $M\!:\!A$ и $N\!:\!B$ . Проекции пары задаются функциями

{\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

{\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

Эти функции удовлетворяют естественным требованиям ${\mathtt {fst}}\,A\,B\,\langle M;N\rangle =M$ и ${\mathtt {snd}}\,A\,B\,\langle M;N\rangle =N$ .

Тип суммы. Для произвольных типов $A$ и $B$ тип их суммы

A+B~\equiv ~\forall \alpha .~(A\to \alpha )\to (B\to \alpha )\to \alpha

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

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

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

Здесь $M\!:\!A$ , $N\!:\!B$ . Функция, осуществляющая разбор случаев (сопоставление с образцом), имеет вид

{\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

Эта функция удовлетворяет следующим естественным требованиям

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

и

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

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

Числа Чёрча. Тип натуральных чисел в системе F

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

населён бесконечным количеством различных элементов, получаемых посредством двух конструкторов ${\mathtt {zero}}\!:\!{\mathtt {Nat}}$ и ${\mathtt {succ}}\!:\!{\mathtt {Nat}}\to {\mathtt {Nat}}$ :

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

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

Натуральное число $n$ может быть получено $n$ -кратным применением второго конструктора к первому или, эквивалентно, представлено термом

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

Свойства

Просто типизированная система обладает свойством типовой безопасности: при $\beta$ -редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.

В своей диссертации Жан-Ив Жирар показал[1], что Система F обладает свойством сильной нормализации: любой допустимый терм за конечное число $\beta$ -редукций приводится к единственной нормальной форме.

Система F является импредикативной системой, поскольку переменная типа, связываемая квантором всеобщности при определении универсального типа, может замещаться самим определяемым объектом. Например, терм ${\texttt {id}}$ единичного типа $\top \equiv \forall \alpha .~\alpha \to \alpha$ может быть применён к собственному типу, порождая терм типа $\top \to \top$ . Как показал Джо Уэллс в 1994 году[3], задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера.

Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской логикой высказываний второго порядка, формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения $\top$ (истина), $\bot$ (ложь), связки $\lnot$ (отрицание), $\land$ (конъюнкция) и $\lor$ (дизъюнкция), а также $\exists$ (квантор существования) могут быть определены так

\top ~\equiv ~\forall \alpha .\,\alpha \to \alpha

\bot ~\equiv ~\forall \alpha .\,\alpha

\lnot A~\equiv ~A\to \bot

A\land B~\equiv ~\forall \alpha .\,(A\to B\to \alpha )\to \alpha

A\lor B~\equiv ~\forall \alpha .\,(A\to \alpha )\to (B\to \alpha )\to \alpha

\exists \alpha .\,M[\alpha ]~\equiv ~\forall \gamma .\,(\forall \alpha .\,M[\alpha ]\to \gamma )\to \gamma

Отметим, что соответствие Карри — Ховарда ставит в соответствие истине — единичный тип, лжи — пустой тип, конъюнкции — произведение типов, а дизъюнкции — их сумму.

Примечания

Girard, Jean-Yves. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur : Ph.D. thesis. — Université Paris 7, 1972.
John C. Reynolds. Towards a Theory of Type Structure. — 1974.
Wells J. B. Typability and type checking in the second-order lambda-calculus are equivalent and undecidable // 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.
- Перевод на русский язык: Пирс Б. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.
Barendregt, Henk. Lambda Calculi with Types // Handbook of Logic in Computer Science. — Oxford University Press, 1992. — Т. II. — С. 117-309.
Jean-Yves Girard, Paul Taylor, Yves Lafont. Proofs and Types. — Cambridge University Press, 1989. — ISBN 0 521 37181 3.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[Girard72-1] Girard, Jean-Yves. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur : Ph.D. thesis. — Université Paris 7, 1972.

[Reynolds74-2] John C. Reynolds. Towards a Theory of Type Structure. — 1974.

[Wells94-3] Wells J. B. Typability and type checking in the second-order lambda-calculus are equivalent and undecidable // Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). — 1994. — С. 176–185.