Система 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$ присутствует с типом $A$ в контексте $\mathrm{\Gamma }$, то в этом контексте $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$ присутствует с типом $A$ в контексте $\mathrm{\Gamma }$, то в этом контексте $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 }$. Как показал Джо Уэллс в 1994 году, задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера.

• Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской Шаблон:Не переведено, формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения $\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$

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

Литература

• Шаблон:Книга
  • Перевод на русский язык: Шаблон:Книга
• Шаблон:Статья
• Шаблон:Книга