Система F (полиморфное лямбда-исчисление, система
, типизированное лямбда-исчисление второго порядка) — система типизированного лямбда-исчисления,
отличающаяся от просто типизированной системы наличием механизма универсальной квантификации над типами. Эту систему разработал в 1972 году Жан-Ив Жирар [1] в контексте теории доказательств в логике. Независимо от него подобную систему предложил в 1974 году Джон Рейнольдс[2]. Система F позволяет формализовать концепцию параметрического полиморфизма в языках программирования и служит теоретической основой для таких языков программирования как Haskell и ML.
Система F допускает конструирование термов, зависящих от типов. Технически это достигается через механизм абстрагирования терма по типу, что в результате даёт новый терм. Традиционно для такой абстракции используют символ большой лямбды
. Например, взяв терм
типа
и абстрагируясь по переменной типа
, получаем терм
. Этот терм представляет собой функцию из типов в термы. Применяя эту функцию к различным типам, мы будем получать термы с идентичной структурой, но разными типами:
— терм типа
;
— терм типа
.
Видно, что терм
обладает полиморфным поведением, то есть задаёт общий интерфейс для различных типов данных. В Системе F этому терму приписывается тип
. Квантор всеобщности в типе подчёркивает возможность подстановки вместо переменной типа
любого допустимого типа.
Формальное описание
Синтаксис типов
Типы Системы F конструируются из набора переменных типа с помощью операторов
и
. По традиции для переменных типа используют греческие буквы. Правила формирования типов таковы:
- (Переменная типа) Если
— переменная типа, то
— это тип;
- (Стрелочный тип) Если
и
являются типами, то
— это тип;
- (Универсальный тип) Если
является переменной типа, а
— типом, то
— это тип.
Внешние скобки часто опускают, оператор
считают правоассоциативным, а действие оператора
продолжающимся вправо насколько это возможно. Например,
— стандартное сокращение для
.
Синтаксис термов
Термы Системы F конструируются из набора термовых переменных (
,
,
и т.д.) по следующим правилам
- (Переменная) Если
— переменная, то
— это терм;
- (Абстракция) Если
является переменной,
— типом, а
— термом, то
— это терм;
- (Применение) Если
и
являются термами, то
— это терм;
- (Универсальная абстракция) Если
является переменной типа, а
— термом, то
— это терм;
- (Универсальное применение) Если
является термом, а
— типом, то
— это терм.
Внешние скобки часто опускают, оба сорта применения считают левоассоциативными, а действие абстракций — продолжающимся вправо насколько это возможно.
Различают две версии просто типизированной системы. Если, как в приведённых выше правилах, термовые переменные в лямбда-абстракции аннотируются типами, то систему называют типизированной по Чёрчу. Если же правило абстракции заменить на
- (Абстракция по Карри) Если
является переменной, а
— термом, то
— это терм,
и отбросить два последних правила, то систему называют типизированной по Карри. Фактически, термы системы, типизированной по Карри, те же, что и в бестиповом лямбда-исчислении.
Правила редукции
Помимо стандартного для лямбда-исчисления правила
-редукции
![{\displaystyle (\lambda a^{A}.~M)~N\ \to _{\beta }\ M[a:=N]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/154fd8e28a0e3e57e44b5387bfa351fbacf59a3a)
в системе F в стиле Чёрча вводится дополнительное правило,
,
позволяющее вычислять применение терма к типу через механизм подстановки типа вместо переменной типа.
Контексты типизации и утверждение типизации
Контекстом, как и в просто типизированном лямбда-исчислении, называется множество утверждений о приписывании типов различным переменным, разделённых запятой
![{\displaystyle \Gamma =x_{1}\!:\!A_{1},x_{2}\!:\!A_{1},\ldots ,x_{n}\!:\!A_{n}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4c67fce4d78b6369dfff7f669fad5d8267b6f71)
В контекст можно добавить «свежую» для этого контекста переменную: если
— допустимый контекст, не содержащий переменной
, а
— тип, то
— тоже допустимый контекст.
Общий вид утверждения о типизации таков:
![{\displaystyle \Gamma \vdash M\!:\!A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f2600857f6a91c56805cb4592cda1515f079d7c)
Это читается следующим образом: в контексте
терм
имеет тип
.
Правила типизации по Чёрчу
В Системе F, типизированной по Чёрчу, приписывание типов термам осуществляется в соответствии со следующими правилами:
(Начальное правило) Если переменная
присутствует с типом
в контексте
, то в этом контексте
имеет тип
. В виде правила вывода
|
(Правило введения
) Если в некотором контексте, расширенном утверждением, что
имеет тип
, терм
имеет тип
, то в упомянутом контексте (без
), лямбда-абстракция
имеет тип
. В виде правила вывода
|
(Правило удаления
) Если в некотором контексте терм
имеет тип
, а терм
имеет тип
, то применение
имеет тип
. В виде правила вывода
|
(Правило введения
) Если в некотором контексте терм
имеет тип
, то в этом контексте терм
имеет тип
. В виде правила вывода
|
Это правило требует оговорки: переменная типа
не должна встречаться в утверждениях типизации контекста
.
(Правило удаления
) Если в некотором контексте терм
имеет тип
, и
— это тип, то в этом контексте терм
имеет тип
. В виде правила вывода
|
Правила типизации по Карри
В Системе F, типизированной по Карри, приписывание типов термам осуществляется в соответствии со следующими правилами:
(Начальное правило) Если переменная
присутствует с типом
в контексте
, то в этом контексте
имеет тип
. В виде правила вывода
|
(Правило введения
) Если в некотором контексте, расширенном утверждением, что
имеет тип
, терм
имеет тип
, то в упомянутом контексте (без
), лямбда-абстракция
имеет тип
. В виде правила вывода
|
(Правило удаления
) Если в некотором контексте терм
имеет тип
, а терм
имеет тип
, то применение
имеет тип
. В виде правила вывода
|
(Правило введения
) Если в некотором контексте терм
имеет тип
, то в этом контексте этому терму
может быть приписан и тип
. В виде правила вывода
|
Это правило требует оговорки: переменная типа
не должна встречаться в утверждениях типизации контекста
.
(Правило удаления
) Если в некотором контексте терм
имеет тип
, и
— это тип, то в этом контексте этому терму
может быть приписан и тип
. В виде правила вывода
|
Пример. По начальному правилу:
![{\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d5540e1bfac30468b60220503b43497fe44192b8)
Применим правило удаления
, взяв в качестве
тип
![{\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash x\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ed5b9c06decf0122ebce032557dd236779158453)
Теперь по правилу удаления
имеем возможность применить терм
сам к себе
![{\displaystyle x\!:\!(\forall \alpha .~\alpha \to \alpha )\vdash (x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc89f1b5d079643f7b22d47d4b300ecea4527d32)
и, наконец, по правилу введения
![{\displaystyle \vdash (\lambda x.~x~x)\!:\!(\forall \alpha .~\alpha \to \alpha )\to (\forall \alpha .~\alpha \to \alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/359032ff85ae77efd3d5e207f29ba131c5a7ddc9)
Это пример терма, типизируемого в Системе F, но не в просто типизированной системе.
Представление типов данных
Система F обладает достаточными выразительными средствами, для того чтобы напрямую реализовать многие типы данных, используемые в языках программирования. Будем работать в версии Чёрча системы F.
Пустой тип. Тип
![{\displaystyle \bot \ \equiv \ \forall \alpha .~\alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/befee1ce5e552b2623db8df7c76edb04b7b2beed)
необитаем в системе F, то есть в ней отсутствуют термы с таким типом.
Единичный тип. У типа
![{\displaystyle \top \ \equiv \ \forall \alpha .~\alpha \to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/63f83b054b31001dee0f207869616ceeb762e662)
в системе F имеется единственный находящийся в нормальной форме обитатель — терм
.
Булев тип. В системе F задается так:
.
У этого типа ровно два обитателя, отождествляемых с двумя булевыми константами
![{\displaystyle {\mathtt {true}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~x}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c89424be7e51ad294ee7c742288e042c5f806a2b)
![{\displaystyle {\mathtt {false}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~y}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b5a46012956ef0092a1381d9f25d210ba5e6ab8f)
Конструкция условного оператора
![{\displaystyle {\mathtt {ifThenElse}}\ \equiv \ \Lambda \alpha .~\lambda b^{\mathtt {Bool}}.~\lambda x^{\alpha }.~\lambda y^{\alpha }.~b\,\alpha \,x\,y}](https://wikimedia.org/api/rest_v1/media/math/render/svg/69765b80478131814adbe47469301555a507db08)
Эта функция удовлетворяет естественным требованиям
![{\displaystyle {\mathtt {ifThenElse}}\,A\,{\mathtt {true}}\,M\,N=M}](https://wikimedia.org/api/rest_v1/media/math/render/svg/458a3828350ac775676d29b47892e62b0c6fb02f)
и
![{\displaystyle {\mathtt {ifThenElse}}\,A\,{\mathtt {false}}\,M\,N=N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ac13617774503a288a99044f60dbbf804eaac9cf)
для произвольного типа
и произвольных
и
. В этом легко убедиться, раскрыв определения и выполнив
-редукции.
Тип произведения. Для произвольных типов
и
тип их декартова произведения
![{\displaystyle A\times B~\equiv ~\forall \alpha .~(A\to B\to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/58abe456f94c28adabe0ccc855c15336cde4eacc)
населён парой
![{\displaystyle \langle M;N\rangle ~\equiv ~\Lambda \alpha .~\lambda f^{(A\to B\to \alpha )}.~f~M~N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/35502f72922c81d9ac3410a65f62070b1b797b3a)
для каждых
и
. Проекции пары задаются функциями
![{\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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/1866f1804caa00825282fb229236fded8e36d231)
![{\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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/c099795a0ebcb20e873179d4bd6ceecbffd00373)
Эти функции удовлетворяют естественным требованиям
и
.
Тип суммы. Для произвольных типов
и
тип их суммы
![{\displaystyle A+B~\equiv ~\forall \alpha .~(A\to \alpha )\to (B\to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/6de7cb764b841c6a957d8d3b758e774bfec606c7)
населён либо термом типа
, либо термом типа
, в зависимости от применённого конструктора
![{\displaystyle {\mathtt {injL}}\,M~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }.\,f\,M}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3567d6a2119a4f0ad188fa90c163be8f24e5def9)
![{\displaystyle {\mathtt {injR}}\,N~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }.\,g\,N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aa9957c8d8754ae33e2cde3d69c99df70e101d85)
Здесь
,
.
Функция, осуществляющая разбор случаев (сопоставление с образцом), имеет вид
![{\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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/f8311c58e757435dce68e677ad28ef7e9ea1ca43)
Эта функция удовлетворяет следующим естественным требованиям
![{\displaystyle {\mathtt {match}}\,A\,B\,C\,({\mathtt {injL}}\,M)\,F\,G=F\,M}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bbe3b1b9dd4aac3089b13b1dbaa5f5c060c0ee3f)
и
![{\displaystyle {\mathtt {match}}\,A\,B\,C\,({\mathtt {injR}}\,N)\,F\,G=G\,N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/947e1b55549469d3576c753ec642fd1c6859fbb0)
для произвольных типов
,
и
и произвольных термов
и
.
Числа Чёрча. Тип натуральных чисел в системе F
![{\displaystyle {\mathtt {Nat}}\ \equiv \ \forall \alpha .~\alpha \to (\alpha \to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/cdb2bb94d49604a2b6f0f4815407ba2e1219f052)
населён бесконечным количеством различных элементов, получаемых посредством двух конструкторов
и
:
![{\displaystyle {\mathtt {zero}}\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,z}](https://wikimedia.org/api/rest_v1/media/math/render/svg/335b340f8437669a209cd9c5567c1b5e664c8931)
![{\displaystyle {\mathtt {succ}}\ \equiv \ \lambda n^{\mathtt {Nat}}.\,\Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,s\,(n\,\alpha \,z\,s)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ccaff29aff61287ad3507f67cf9cfa6259e83bd)
Натуральное число
может быть получено
-кратным применением второго конструктора к первому или, эквивалентно, представлено термом
![{\displaystyle {\overline {n}}\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \rightarrow \alpha }.\,\underbrace {s(s(s\ldots (s} _{n}\,z)\ldots ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d742f3b5197cc598efb69d91ebe7d9805cd22fb3)
Свойства
- Просто типизированная система обладает свойством типовой безопасности: при
-редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.
- В своей диссертации Жан-Ив Жирар показал[1], что Система F обладает свойством сильной нормализации: любой допустимый терм за конечное число
-редукций приводится к единственной нормальной форме.
- Система F является импредикативной[англ.] системой, поскольку переменная типа, связываемая квантором всеобщности при определении универсального типа, может замещаться самим определяемым объектом. Например, терм
единичного типа
может быть применён к собственному типу, порождая терм типа
. Как показал Джо Уэллс в 1994 году[3], задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера.
- Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской логикой высказываний второго порядка[англ.], формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения
(истина),
(ложь), связки
(отрицание),
(конъюнкция) и
(дизъюнкция), а также
(квантор существования) могут быть определены так
![{\displaystyle \top ~\equiv ~\forall \alpha .\,\alpha \to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/8eef891729e0c009a80334f213ac111660a8c6e8)
![{\displaystyle \bot ~\equiv ~\forall \alpha .\,\alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc9c68ba07b1b3fbcb36fa6e1929e0f599d85fe8)
![{\displaystyle \lnot A~\equiv ~A\to \bot }](https://wikimedia.org/api/rest_v1/media/math/render/svg/ae988a96ea0b8c359706cd0ac1bc0ed098e63fbb)
![{\displaystyle A\land B~\equiv ~\forall \alpha .\,(A\to B\to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ed9333f4930ecc2ffb620d993b4fb1b58a4eadc)
![{\displaystyle A\lor B~\equiv ~\forall \alpha .\,(A\to \alpha )\to (B\to \alpha )\to \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/a1347ecd1951bf3208fc954b68e3b81e0d1447ea)
![{\displaystyle \exists \alpha .\,M[\alpha ]~\equiv ~\forall \gamma .\,(\forall \alpha .\,M[\alpha ]\to \gamma )\to \gamma }](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1a7cd018093ccc25534e9938eb1a9d4bf039ba1)
Отметим, что соответствие Карри — Ховарда ставит в соответствие истине — единичный тип, лжи — пустой тип, конъюнкции — произведение типов, а дизъюнкции — их сумму.
Примечания
Литература