Система F

Типизированное лямбда-исчисление

Система F (также полиморфное лямбда-исчисление или лямбда-исчисление второго порядка ) — типизированное лямбда-исчисление , которое вводит в простое типизированное лямбда-исчисление механизм универсальной квантификации по типам. Система F формализует параметрический полиморфизм в языках программирования , тем самым формируя теоретическую основу для таких языков, как Haskell и ML . Она была открыта независимо логиком Жаном-Ивом Жираром (1972) и компьютерным ученым Джоном К. Рейнольдсом .

В то время как просто типизированное лямбда-исчисление имеет переменные, ранжирующиеся по терминам, и связующие элементы для них, Система F дополнительно имеет переменные, ранжирующиеся по типам , и связующие элементы для них. Например, тот факт, что функция тождества может иметь любой тип формы A → A, будет формализован в Системе F как суждение

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

где — переменная типа . Верхний регистр традиционно используется для обозначения функций уровня типа, в отличие от нижнего регистра , который используется для функций уровня значения. (Верхний индекс означает, что граница x имеет тип ; выражение после двоеточия — это тип лямбда-выражения, предшествующего ему.) ${\displaystyle \alpha }$ ${\displaystyle \Lambda }$ ${\displaystyle \lambda }$ ${\displaystyle \alpha }$ ${\displaystyle \alpha }$

Как система переписывания терминов , система F является строго нормализующей . Однако вывод типов в системе F (без явных аннотаций типов) неразрешим. При изоморфизме Карри–Ховарда система F соответствует фрагменту интуиционистской логики второго порядка , которая использует только универсальную квантификацию. Систему F можно рассматривать как часть лямбда-куба вместе с еще более выразительными типизированными лямбда-исчислениями, включая те, которые имеют зависимые типы .

По словам Жирара, буква «F» в аббревиатуре System F была выбрана случайно. ^[1]

Правила набора текста

Правила типизации Системы F аналогичны правилам простого типизированного лямбда-исчисления с добавлением следующего:

где есть типы, есть переменная типа, а в контексте указывает, что связан. Первое правило — это правило применения, а второе — правило абстракции. ^{[2] [3]} ${\displaystyle \sigma ,\tau }$ ${\displaystyle \alpha }$ ${\displaystyle \alpha ~{\text{type}}}$ ${\displaystyle \alpha }$

Логика и предикаты

Тип определяется как: , где — переменная типа . Это означает: — тип всех функций, которые принимают на входе тип α и два выражения типа α, и производят на выходе выражение типа α (обратите внимание, что мы считаем его правоассоциативным . ) ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle \to }$

Используются следующие два определения для булевых значений , расширяющие определение булевых значений Чёрча : ${\displaystyle \mathbf {T} }$ ${\displaystyle \mathbf {F} }$

${\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}$

(Обратите внимание, что две приведенные выше функции требуют трех — а не двух — аргументов. Последние два должны быть лямбда-выражениями, но первый должен быть типом. Этот факт отражен в том факте, что тип этих выражений — ; квантор всеобщности, связывающий α, соответствует Λ, связывающему альфа в самом лямбда-выражении. Также обратите внимание, что — удобное сокращение для , но это не символ самой системы F, а скорее «мета-символ». Аналогично, и также являются «мета-символами», удобными сокращениями «сборок» системы F (в смысле Бурбаки); в противном случае, если бы такие функции могли быть названы (в системе F), то не было бы необходимости в аппарате лямбда-выражений, способном определять функции анонимно, и в комбинаторе с фиксированной точкой , который работает в обход этого ограничения.) ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$ ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$ ${\displaystyle \mathbf {T} }$ ${\displaystyle \mathbf {F} }$

Затем с помощью этих двух -термов мы можем определить некоторые логические операторы (которые имеют тип ): ${\displaystyle \lambda }$ ${\displaystyle {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}}$

${\displaystyle {\begin{aligned}\mathrm {AND} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {F} \,\mathbf {T} \end{aligned}}}$

Обратите внимание, что в определениях выше, является аргументом типа для , указывающим, что два других параметра, которые заданы для , имеют тип . Как и в кодировках Чёрча, нет необходимости в функции IFTHENELSE , поскольку можно просто использовать необработанные типизированные термины в качестве функций принятия решений. Однако, если запрошено: ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle {\mathsf {Boolean}}}$

${\displaystyle \mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

будет делать. Предикат — это функция, которая возвращает типизированное значение. Самый фундаментальный предикат — ISZERO , который возвращает значение только в том случае, если его аргумент — это число Чёрча 0 : ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle \mathbf {T} }$

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T} }$

Структуры системы F

Система F позволяет встраивать рекурсивные конструкции естественным образом, как в теории типов Мартина-Лёфа . Абстрактные структуры ( S ) создаются с помощью конструкторов . Это функции, типизированные как:

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$.

Рекурсия проявляется, когда S сам появляется внутри одного из типов . Если у вас есть m таких конструкторов, вы можете определить тип S как: ${\displaystyle K_{i}}$

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

Например, натуральные числа можно определить как индуктивный тип данных N с конструкторами

${\displaystyle {\begin{aligned}{\mathit {zero}}&:\mathrm {N} \\{\mathit {succ}}&:\mathrm {N} \rightarrow \mathrm {N} \end{aligned}}}$

Тип системы F, соответствующий этой структуре, — . Термины этого типа включают в себя типизированную версию числительных Чёрча , первые несколько из которых: ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$

${\displaystyle {\begin{aligned}0&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x\\1&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx\\2&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))\end{aligned}}}$

Если мы изменим порядок каррированных аргументов ( т.е. ), то число Чёрча для n будет функцией, которая принимает функцию f в качестве аргумента и возвращает n ^-ю степень f . То есть число Чёрча будет функцией более высокого порядка — она принимает функцию f с одним аргументом и возвращает другую функцию с одним аргументом. ${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$

Использование в языках программирования

Версия System F, используемая в этой статье, является явно типизированным исчислением или исчислением в стиле Чёрча. Информация о типизации, содержащаяся в λ-термах, делает проверку типов простой. Джо Уэллс (1994) решил «неловкую открытую проблему», доказав, что проверка типов неразрешима для варианта System F в стиле Карри, то есть для такого, в котором отсутствуют явные аннотации о типизации. ^{[4] [5]}

Результат Уэллса подразумевает, что вывод типа для System F невозможен. Ограничение System F, известное как « Хиндли–Милнер », или просто «HM», имеет простой алгоритм вывода типа и используется для многих статически типизированных функциональных языков программирования , таких как Haskell 98 и семейство ML . Со временем, по мере того как ограничения систем типов в стиле HM становились очевидными, языки неуклонно переходили к более выразительной логике для своих систем типов. GHC , компилятор Haskell, выходит за рамки HM (по состоянию на 2008 год) и использует System F, расширенную с несинтаксическим равенством типов; ^[6] не-HM функции в системе типов OCaml включают GADT . ^{[7] [8]}

Изоморфизм Жирара-Рейнольдса

В интуиционистской логике второго порядка полиморфное лямбда-исчисление второго порядка (F2) было открыто Жираром (1972) и независимо Рейнольдсом (1974). ^[9] Жирар доказал теорему о представлении : что в интуиционистской предикатной логике второго порядка (P2) функции от натуральных чисел до натуральных чисел, которые могут быть доказаны как полные, образуют проекцию из P2 в F2. ^[9] Рейнольдс доказал теорему об абстракции : что каждый член в F2 удовлетворяет логическому отношению, которое может быть встроено в логические отношения P2. ^[9] Рейнольдс доказал, что проекция Жирара, за которой следует вложение Рейнольдса, образуют тождество, т. е. изоморфизм Жирара-Рейнольдса . ^[9]

Система Fω

В то время как система F соответствует первой оси лямбда-куба Барендрегта , система F _ω или полиморфное лямбда-исчисление более высокого порядка объединяет первую ось (полиморфизм) со второй осью ( операторы типа ); это другая, более сложная система.

Систему F _ω можно определить индуктивно на семействе систем, где индукция основана на видах, разрешенных в каждой системе:

• ${\displaystyle F_{n}}$Виды разрешений:
  • ${\displaystyle \star }$(вид типов) и
  • ${\displaystyle J\Rightarrow K}$где и (вид функций из типов в типы, где тип аргумента имеет низший порядок) ${\displaystyle J\in F_{n-1}}$ ${\displaystyle K\in F_{n}}$

В пределе мы можем определить систему как ${\displaystyle F_{\omega }}$

• ${\displaystyle F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}}$

То есть F _ω — это система, которая допускает функции из типов в типы, где аргумент (и результат) может быть любого порядка.

Обратите внимание, что хотя F _ω не накладывает ограничений на порядок аргументов в этих отображениях, она ограничивает универсум аргументов для этих отображений: они должны быть типами, а не значениями. Система F _ω не допускает отображений из значений в типы ( зависимые типы ), хотя она допускает отображения из значений в значения ( абстракция), отображения из типов в значения ( абстракция) и отображения из типов в типы ( абстракция на уровне типов). ${\displaystyle \lambda }$ ${\displaystyle \Lambda }$ ${\displaystyle \lambda }$

Система F

Система F _<: , произносится как «F-sub», является расширением системы F с подтипированием . Система F _<: имеет центральное значение для теории языков программирования с 1980-х годов ^{[ требуется ссылка ],} поскольку ядро ​​функциональных языков программирования , таких как языки семейства ML , поддерживает как параметрический полиморфизм , так и подтипирование записей , что может быть выражено в системе F _<: . ^{[10] [11]}

Смотрите также

• Экзистенциальные типы — экзистенциально квантифицированные аналоги универсальных типов
• Система U
• Лямбда-куб

Примечания

1. Жирар, Жан-Ив (1986). "Система F переменных типов, пятнадцать лет спустя". Теоретическая информатика . 45 : 160. doi :10.1016/0304-3975(86)90044-7. Однако в [3] было показано, что очевидные правила преобразования для этой системы, названной F случайно, сходятся.
2. Харпер Р. «Практические основы языков программирования, второе издание» (PDF) . стр. 142–3.
3. Гейверс Х., Нордстрём Б., Довек Г. «Доказательства программ и формализация математики» (PDF) . стр. 51.
4. Уэллс, Дж. Б. (2005-01-20). «Исследовательские интересы Джо Уэллса». Университет Хериот-Уотт.
5. Уэллс, Дж. Б. (1999). «Типичность и проверка типов в системе F эквивалентны и неразрешимы». Ann. Pure Appl. Logic . 98 (1–3): 111–156. doi : 10.1016/S0168-0072(98)00047-5 .«Проект Чёрча: Типичность и проверка типов в {S}ystem {F} эквивалентны и неразрешимы». 29 сентября 2007 г. Архивировано из оригинала 29 сентября 2007 г.
6. "Системный FC: ограничения равенства и приведения". gitlab.haskell.org . Получено 2019-07-08 .
7. "Заметки о выпуске OCaml 4.00.1". ocaml.org . 2012-10-05 . Получено 2019-09-23 .
8. "Справочное руководство OCaml 4.09". 2012-09-11 . Получено 2019-09-23 .
9. Филип Вадлер (2005) Изоморфизм Жирара-Рейнольдса (второе издание) Эдинбургский университет , Языки программирования и основы в Эдинбурге
10. Карделли, Лука; Мартини, Симоне; Митчелл, Джон К.; Скедров, Андре (1994). «Расширение системы F с подтипированием». Информация и вычисления, т. 9. Северная Голландия, Амстердам. стр. 4–56. doi : 10.1006/inco.1994.1013 .
11. Пирс, Бенджамин (2002). Типы и языки программирования . MIT Press. ISBN 978-0-262-16209-8., Глава 26: Ограниченная квантификация

Ссылки

• Жирар, Жан-Ив (1971). «Расширение интерпретации Гёделя для анализа и его применение для устранения купюр в анализе и теории типов». Материалы Второго скандинавского логического симпозиума . Амстердам. стр. 63–92. дои : 10.1016/S0049-237X(08)70843-7.
• Жирар, Жан-Ив (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre superieur (докторская диссертация) (на французском языке), Парижский университет 7.
• Рейнольдс, Джон (1974). К теории структуры типа (PDF) .
• Жирар, Жан-Ив; Лафон, Ив; Тейлор, Пол (1989). Доказательства и шрифты. Cambridge University Press. ISBN 978-0-521-37181-0.
• Уэллс, Дж. Б. (1994). «Типичность и проверка типов в лямбда-исчислении второго порядка эквивалентны и неразрешимы». Труды 9-го ежегодного симпозиума IEEE по логике в компьютерных науках (LICS) . стр. 176–185. doi :10.1109/LICS.1994.316068. ISBN 0-8186-6310-3.Постскриптум версия

Дальнейшее чтение

• Пирс, Бенджамин (2002). "V Полиморфизм Гл. 23. Универсальные типы, Гл. 25. Реализация системы F на языке ML". Типы и языки программирования . MIT Press. С. 339–362, 381–388. ISBN 0-262-16209-1.

Внешние ссылки

• Краткое изложение Системы F Франка Бинарда.
• Система Fω: рабочая лошадка современных компиляторов Грега Моррисетта