Система F

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

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

[math]\displaystyle{ (\Lambda\alpha.~\lambda x^\alpha.~x)~\texttt{Bool}\ \to_{\beta}\ \lambda x^\texttt{Bool}.~x }[/math] — терм типа [math]\displaystyle{ \texttt{Bool}\to\texttt{Bool} }[/math];

[math]\displaystyle{ (\Lambda\alpha.~\lambda x^\alpha.~x)~\texttt{Nat}\ \to_{\beta}\ \lambda x^\texttt{Nat}.~x }[/math] — терм типа [math]\displaystyle{ \texttt{Nat}\to\texttt{Nat} }[/math].

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

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

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

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

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

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

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

Термы Системы F конструируются из набора термовых переменных ([math]\displaystyle{ x }[/math], [math]\displaystyle{ y }[/math], [math]\displaystyle{ z }[/math] и т.д.) по следующим правилам

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

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

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

• (Абстракция по Карри) Если [math]\displaystyle{ x }[/math] является переменной, а [math]\displaystyle{ M }[/math] — термом, то [math]\displaystyle{ (\lambda x.~M) }[/math] — это терм,

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

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

Помимо стандартного для лямбда-исчисления правила [math]\displaystyle{ \beta }[/math]-редукции

[math]\displaystyle{ (\lambda a^A.~M)~N\ \to_{\beta}\ M[a:=N] }[/math]

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

[math]\displaystyle{ (\Lambda \alpha.~M)~A\ \to_{\beta}\ M[\alpha:=A] }[/math],

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

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

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

[math]\displaystyle{ \Gamma=x_1\!:\!A_1,x_2\!:\!A_1,\ldots,x_n\!:\!A_n }[/math]

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

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

[math]\displaystyle{ \Gamma\vdash M\!:\!A }[/math]

Это читается следующим образом: в контексте [math]\displaystyle{ \Gamma }[/math] терм [math]\displaystyle{ M }[/math] имеет тип [math]\displaystyle{ A }[/math].

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

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

(Начальное правило) Если переменная [math]\displaystyle{ x }[/math] присутствует с типом [math]\displaystyle{ A }[/math] в контексте [math]\displaystyle{ \Gamma }[/math], то в этом контексте [math]\displaystyle{ x }[/math] имеет тип [math]\displaystyle{ A }[/math]. В виде правила вывода

[math]\displaystyle{ {x\!:\!A \in \Gamma}\over{\Gamma \vdash x\!:\!A } }[/math]

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

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

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

[math]\displaystyle{ {\Gamma\vdash M\!:\!(A \to B)\quad\Gamma\vdash N\!:\!A}\over{\Gamma\vdash (M~N)\!:\!B} }[/math]

(Правило введения [math]\displaystyle{ \forall }[/math]) Если в некотором контексте терм [math]\displaystyle{ M }[/math] имеет тип [math]\displaystyle{ A }[/math], то в этом контексте терм [math]\displaystyle{ \Lambda \alpha.~M }[/math] имеет тип [math]\displaystyle{ \forall\alpha.~A }[/math]. В виде правила вывода

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

Это правило требует оговорки: переменная типа [math]\displaystyle{ \alpha }[/math] не должна встречаться в утверждениях типизации контекста [math]\displaystyle{ \Gamma }[/math].

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

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

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

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

(Начальное правило) Если переменная [math]\displaystyle{ x }[/math] присутствует с типом [math]\displaystyle{ A }[/math] в контексте [math]\displaystyle{ \Gamma }[/math], то в этом контексте [math]\displaystyle{ x }[/math] имеет тип [math]\displaystyle{ A }[/math]. В виде правила вывода

[math]\displaystyle{ {x\!:\!A \in \Gamma}\over{\Gamma \vdash x\!:\!A } }[/math]

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

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

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

[math]\displaystyle{ {\Gamma\vdash M\!:\!(A \to B)\quad\Gamma\vdash N\!:\!A}\over{\Gamma\vdash (M~N)\!:\!B} }[/math]

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

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

Это правило требует оговорки: переменная типа [math]\displaystyle{ \alpha }[/math] не должна встречаться в утверждениях типизации контекста [math]\displaystyle{ \Gamma }[/math].

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

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

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

[math]\displaystyle{ x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash x\!:\!(\forall\alpha.~\alpha\to\alpha) }[/math]

Применим правило удаления [math]\displaystyle{ \forall }[/math], взяв в качестве [math]\displaystyle{ B }[/math] тип [math]\displaystyle{ \forall\alpha.~\alpha\to\alpha }[/math]

[math]\displaystyle{ x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash x\!:\!(\forall\alpha.~\alpha\to\alpha)\to(\forall\alpha.~\alpha\to\alpha) }[/math]

Теперь по правилу удаления [math]\displaystyle{ \rightarrow }[/math] имеем возможность применить терм [math]\displaystyle{ x }[/math] сам к себе

[math]\displaystyle{ x\!:\!(\forall\alpha.~\alpha\to\alpha)\vdash (x~x)\!:\!(\forall\alpha.~\alpha\to\alpha) }[/math]

и, наконец, по правилу введения [math]\displaystyle{ \rightarrow }[/math]

[math]\displaystyle{ \vdash (\lambda x.~x~x)\!:\!(\forall\alpha.~\alpha\to\alpha)\to(\forall\alpha.~\alpha\to\alpha) }[/math]

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

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

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

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

[math]\displaystyle{ \bot\ \equiv\ \forall\alpha.~\alpha }[/math]

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

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

[math]\displaystyle{ \top\ \equiv\ \forall\alpha.~\alpha\to\alpha }[/math]

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

[math]\displaystyle{ \mathtt{id}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~x }[/math].

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

[math]\displaystyle{ \mathtt{Bool}\ \equiv\ \forall\alpha.~\alpha\to\alpha\to\alpha }[/math].

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

[math]\displaystyle{ \mathtt{true}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~\lambda y^\alpha.~x }[/math]

[math]\displaystyle{ \mathtt{false}\ \equiv\ \Lambda\alpha.~\lambda x^\alpha.~\lambda y^\alpha.~y }[/math]

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

[math]\displaystyle{ \mathtt{ifThenElse} \ \equiv\ \Lambda\alpha.~\lambda b^{\mathtt{Bool}}.~\lambda x^\alpha.~\lambda y^\alpha.~b\,\alpha\,x\,y }[/math]

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

[math]\displaystyle{ \mathtt{ifThenElse}\,A\,\mathtt{true}\,M\,N=M }[/math]

и

[math]\displaystyle{ \mathtt{ifThenElse}\,A\,\mathtt{false}\,M\,N=N }[/math]

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

Тип произведения. Для произвольных типов [math]\displaystyle{ A }[/math] и [math]\displaystyle{ B }[/math] тип их декартова произведения

[math]\displaystyle{ A\times B~\equiv~\forall\alpha.~(A\to B\to\alpha)\to\alpha }[/math]

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

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

для каждых [math]\displaystyle{ M\!:\!A }[/math] и [math]\displaystyle{ N\!:\!B }[/math]. Проекции пары задаются функциями

[math]\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 }[/math]

[math]\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 }[/math]

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

Тип суммы. Для произвольных типов [math]\displaystyle{ A }[/math] и [math]\displaystyle{ B }[/math] тип их суммы

[math]\displaystyle{ A+B~\equiv~\forall\alpha.~(A\to\alpha)\to(B\to\alpha)\to\alpha }[/math]

населён либо термом типа [math]\displaystyle{ A }[/math], либо термом типа [math]\displaystyle{ B }[/math], в зависимости от применённого конструктора

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

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

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

[math]\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 }[/math]

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

[math]\displaystyle{ \mathtt{match}\,A\,B\,C\,(\mathtt{injL}\,M)\,F\,G=F\,M }[/math]

и

[math]\displaystyle{ \mathtt{match}\,A\,B\,C\,(\mathtt{injR}\,N)\,F\,G=G\,N }[/math]

для произвольных типов [math]\displaystyle{ A }[/math], [math]\displaystyle{ B }[/math] и [math]\displaystyle{ C }[/math] и произвольных термов [math]\displaystyle{ F\!:\!A\to C }[/math] и [math]\displaystyle{ G\!:\!B\to C }[/math].

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

[math]\displaystyle{ \mathtt{Nat}\ \equiv\ \forall\alpha.~\alpha\to(\alpha\to\alpha)\to\alpha }[/math]

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

[math]\displaystyle{ \mathtt{zero}\ \equiv\ \Lambda\alpha.\,\lambda z^{\alpha}.\,\lambda s^{\alpha\to\alpha}.\,z }[/math]

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

Натуральное число [math]\displaystyle{ n }[/math] может быть получено [math]\displaystyle{ n }[/math]-кратным применением второго конструктора к первому или, эквивалентно, представлено термом

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

Свойства

• Просто типизированная система обладает свойством типовой безопасности: при [math]\displaystyle{ \beta }[/math]-редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.

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

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

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

[math]\displaystyle{ \top~\equiv~\forall\alpha.\,\alpha\to\alpha }[/math]

[math]\displaystyle{ \bot~\equiv~\forall\alpha.\,\alpha }[/math]

[math]\displaystyle{ \lnot A~\equiv~A\to\bot }[/math]

[math]\displaystyle{ A\land B~\equiv~\forall\alpha.\,(A\to B\to\alpha)\to\alpha }[/math]

[math]\displaystyle{ A\lor B~\equiv~\forall\alpha.\,(A\to\alpha)\to(B\to\alpha)\to\alpha }[/math]

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

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

Литература

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