Система F

---

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

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

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

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

---