Система F

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

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

( Λ α . λ x α . x ) Bool → β λ x Bool . x {displaystyle (Lambda alpha .~lambda x^{alpha }.~x)~{ exttt {Bool}} o _{eta } lambda x^{ exttt {Bool}}.~x} — терм типа Bool → Bool {displaystyle { exttt {Bool}} o { exttt {Bool}}} ; ( Λ α . λ x α . x ) Nat → β λ x Nat . x {displaystyle (Lambda alpha .~lambda x^{alpha }.~x)~{ exttt {Nat}} o _{eta } lambda x^{ exttt {Nat}}.~x} — терм типа Nat → Nat {displaystyle { exttt {Nat}} o { exttt {Nat}}} .

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

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

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

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

(Переменная типа) Если α {displaystyle alpha } — переменная типа, то α {displaystyle alpha } — это тип;
(Стрелочный тип) Если A {displaystyle A} и B {displaystyle B} являются типами, то ( A → B ) {displaystyle (A o B)} — это тип;
(Универсальный тип) Если α {displaystyle alpha } является переменной типа, а B {displaystyle B} — типом, то ( ∀ α . B ) {displaystyle (forall alpha .~B)} — это тип.

Внешние скобки часто опускают, оператор → {displaystyle ightarrow } считают правоассоциативным, а действие оператора ∀ {displaystyle forall } продолжающимся вправо насколько это возможно. Например, ∀ α . ∀ β . α → β → α {displaystyle forall alpha .~forall eta .~alpha o eta o alpha } — стандартное сокращение для ( ∀ α . ( ∀ β . ( α → ( β → α ) ) ) ) {displaystyle (forall alpha .~(forall eta .~(alpha o (eta o alpha ))))} .

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

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

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

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

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

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

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

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

Помимо стандартного для лямбда-исчисления правила β {displaystyle eta } -редукции

( λ a A . M ) N → β M [ a := N ] {displaystyle (lambda a^{A}.~M)~N o _{eta } M[a:=N]}

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

( Λ α . M ) A → β M [ α := A ] {displaystyle (Lambda alpha .~M)~A o _{eta } M[alpha :=A]} ,

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

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

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

Γ = x 1 : A 1 , x 2 : A 1 , … , x n : A n {displaystyle Gamma =x_{1}!:!A_{1},x_{2}!:!A_{1},ldots ,x_{n}!:!A_{n}}

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

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

Γ ⊢ M : A {displaystyle Gamma vdash M!:!A}

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

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

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

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

(Правило введения → {displaystyle ightarrow } ) Если в некотором контексте, расширенном утверждением, что a {displaystyle a} имеет тип A {displaystyle A} , терм M {displaystyle M} имеет тип B {displaystyle B} , то в упомянутом контексте (без a {displaystyle a} ), лямбда-абстракция λ a A . M {displaystyle lambda a^{A}.~M} имеет тип A → B {displaystyle A o B} . В виде правила вывода

(Правило удаления → {displaystyle ightarrow } ) Если в некотором контексте терм M {displaystyle M} имеет тип A → B {displaystyle A o B} , а терм N {displaystyle N} имеет тип A {displaystyle A} , то применение M N {displaystyle M~N} имеет тип B {displaystyle B} . В виде правила вывода

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

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

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

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

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

(Правило введения → {displaystyle ightarrow } ) Если в некотором контексте, расширенном утверждением, что a {displaystyle a} имеет тип A {displaystyle A} , терм M {displaystyle M} имеет тип B {displaystyle B} , то в упомянутом контексте (без a {displaystyle a} ), лямбда-абстракция λ a . M {displaystyle lambda a.~M} имеет тип A → B {displaystyle A o B} . В виде правила вывода

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

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

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

x : ( ∀ α . α → α ) ⊢ x : ( ∀ α . α → α ) {displaystyle x!:!(forall alpha .~alpha o alpha )vdash x!:!(forall alpha .~alpha o alpha )}

Применим правило удаления ∀ {displaystyle forall } , взяв в качестве B {displaystyle B} тип ∀ α . α → α {displaystyle forall alpha .~alpha o alpha }

x : ( ∀ α . α → α ) ⊢ x : ( ∀ α . α → α ) → ( ∀ α . α → α ) {displaystyle x!:!(forall alpha .~alpha o alpha )vdash x!:!(forall alpha .~alpha o alpha ) o (forall alpha .~alpha o alpha )}

Теперь по правилу удаления → {displaystyle ightarrow } имеем возможность применить терм x {displaystyle x} сам к себе

x : ( ∀ α . α → α ) ⊢ ( x x ) : ( ∀ α . α → α ) {displaystyle x!:!(forall alpha .~alpha o alpha )vdash (x~x)!:!(forall alpha .~alpha o alpha )}

и, наконец, по правилу введения → {displaystyle ightarrow }

⊢ ( λ x . x x ) : ( ∀ α . α → α ) → ( ∀ α . α → α ) {displaystyle vdash (lambda x.~x~x)!:!(forall alpha .~alpha o alpha ) o (forall alpha .~alpha o alpha )}

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

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

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

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

⊥ ≡ ∀ α . α {displaystyle ot equiv forall alpha .~alpha }

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

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

⊤ ≡ ∀ α . α → α {displaystyle op equiv forall alpha .~alpha o alpha }

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

i d ≡ Λ α . λ x α . x {displaystyle {mathtt {id}} equiv Lambda alpha .~lambda x^{alpha }.~x} .

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

B o o l ≡ ∀ α . α → α → α {displaystyle {mathtt {Bool}} equiv forall alpha .~alpha o alpha o alpha } .

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

t r u e ≡ Λ α . λ x α . λ y α . x {displaystyle {mathtt {true}} equiv Lambda alpha .~lambda x^{alpha }.~lambda y^{alpha }.~x} f a l s e ≡ Λ α . λ x α . λ y α . y {displaystyle {mathtt {false}} equiv Lambda alpha .~lambda x^{alpha }.~lambda y^{alpha }.~y}

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

i f T h e n E l s e ≡ Λ α . λ b B o o l . λ x α . λ y α . b α x y {displaystyle {mathtt {ifThenElse}} equiv Lambda alpha .~lambda b^{mathtt {Bool}}.~lambda x^{alpha }.~lambda y^{alpha }.~b,alpha ,x,y}

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

i f T h e n E l s e A t r u e M N = M {displaystyle {mathtt {ifThenElse}},A,{mathtt {true}},M,N=M}

i f T h e n E l s e A f a l s e M N = N {displaystyle {mathtt {ifThenElse}},A,{mathtt {false}},M,N=N}

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

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

A × B ≡ ∀ α . ( A → B → α ) → α {displaystyle A imes B~equiv ~forall alpha .~(A o B o alpha ) o alpha }

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

⟨ M ; N ⟩ ≡ Λ α . λ f ( A → B → α ) . f M N {displaystyle langle M;N angle ~equiv ~Lambda alpha .~lambda f^{(A o B o alpha )}.~f~M~N}

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

f s t ≡ Λ α . Λ β . λ p α × β . p α ( λ x α . λ y β . x ) : ∀ α . ∀ β . α × β → α {displaystyle {mathtt {fst}} equiv Lambda alpha .~Lambda eta .~lambda p^{alpha imes eta }.~p,alpha ,(lambda x^{alpha }.,lambda y^{eta }.,x)~:~forall alpha .~forall eta .,alpha imes eta o alpha } s n d ≡ Λ α . Λ β . λ p α × β . p β ( λ x α . λ y β . y ) : ∀ α . ∀ β . α × β → β {displaystyle {mathtt {snd}} equiv Lambda alpha .~Lambda eta .~lambda p^{alpha imes eta }.~p,eta ,(lambda x^{alpha }.,lambda y^{eta }.,y)~:~forall alpha .~forall eta .,alpha imes eta o eta }

Эти функции удовлетворяют естественным требованиям f s t A B ⟨ M ; N ⟩ = M {displaystyle {mathtt {fst}},A,B,langle M;N angle =M} и s n d A B ⟨ M ; N ⟩ = N {displaystyle {mathtt {snd}},A,B,langle M;N angle =N} .

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

A + B ≡ ∀ α . ( A → α ) → ( B → α ) → α {displaystyle A+B~equiv ~forall alpha .~(A o alpha ) o (B o alpha ) o alpha }

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

i n j L M ≡ Λ α . λ f A → α . λ g B → α . f M {displaystyle {mathtt {injL}},M~equiv ~Lambda alpha .,lambda f^{A o alpha }.,lambda g^{B o alpha }.,f,M} i n j R N ≡ Λ α . λ f A → α . λ g B → α . g N {displaystyle {mathtt {injR}},N~equiv ~Lambda alpha .,lambda f^{A o alpha }.,lambda g^{B o alpha }.,g,N}

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

m a t c h ≡ Λ α . Λ β . Λ γ . λ s α + β . λ f α → γ . λ g β → γ . s γ f g : ∀ α . ∀ β . ∀ γ . α + β → ( α → γ ) → ( β → γ ) → γ {displaystyle {mathtt {match}}~equiv ~Lambda alpha .,Lambda eta .,Lambda gamma .,lambda s^{alpha +eta }.,lambda f^{alpha o gamma }.,lambda g^{eta o gamma }.,s,gamma ,f,g~:~forall alpha .~forall eta .~forall gamma .~alpha +eta o (alpha o gamma ) o (eta o gamma ) o gamma }

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

m a t c h A B C ( i n j L M ) F G = F M {displaystyle {mathtt {match}},A,B,C,({mathtt {injL}},M),F,G=F,M}

m a t c h A B C ( i n j R N ) F G = G N {displaystyle {mathtt {match}},A,B,C,({mathtt {injR}},N),F,G=G,N}

для произвольных типов A {displaystyle A} , B {displaystyle B} и C {displaystyle C} и произвольных термов F : A → C {displaystyle F!:!A o C} и G : B → C {displaystyle G!:!B o C} .

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

N a t ≡ ∀ α . α → ( α → α ) → α {displaystyle {mathtt {Nat}} equiv forall alpha .~alpha o (alpha o alpha ) o alpha }

населён бесконечным количеством различных элементов, получаемых посредством двух конструкторов z e r o : N a t {displaystyle {mathtt {zero}}!:!{mathtt {Nat}}} и s u c c : N a t → N a t {displaystyle {mathtt {succ}}!:!{mathtt {Nat}} o {mathtt {Nat}}} :

z e r o ≡ Λ α . λ z α . λ s α → α . z {displaystyle {mathtt {zero}} equiv Lambda alpha .,lambda z^{alpha }.,lambda s^{alpha o alpha }.,z} s u c c ≡ λ n N a t . Λ α . λ z α . λ s α → α . s ( n α z s ) {displaystyle {mathtt {succ}} equiv lambda n^{mathtt {Nat}}.,Lambda alpha .,lambda z^{alpha }.,lambda s^{alpha o alpha }.,s,(n,alpha ,z,s)}

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

n ¯ ≡ Λ α . λ z α . λ s α → α . s ( s ( s … ( s ⏟ n z ) … ) ) {displaystyle {overline {n}} equiv Lambda alpha .,lambda z^{alpha }.,lambda s^{alpha ightarrow alpha }.,underbrace {s(s(sldots (s} _{n},z)ldots ))}

Свойства

Просто типизированная система обладает свойством типовой безопасности: при β {displaystyle eta } -редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.

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

Система F является импредикативной системой, поскольку переменная типа, связываемая квантором всеобщности при определении универсального типа, может замещаться самим определяемым объектом. Например, терм id {displaystyle { exttt {id}}} единичного типа ⊤ ≡ ∀ α . α → α {displaystyle op equiv forall alpha .~alpha o alpha } может быть применён к собственному типу, порождая терм типа ⊤ → ⊤ {displaystyle op o op } . Как показал Джо Уэллс в 1994 году, задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера.

Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской логикой высказываний второго порядка, формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения ⊤ {displaystyle op } (истина), ⊥ {displaystyle ot } (ложь), связки ¬ {displaystyle lnot } (отрицание), ∧ {displaystyle land } (конъюнкция) и ∨ {displaystyle lor } (дизъюнкция), а также ∃ {displaystyle exists } (квантор существования) могут быть определены так

⊤ ≡ ∀ α . α → α {displaystyle op ~equiv ~forall alpha .,alpha o alpha } ⊥ ≡ ∀ α . α {displaystyle ot ~equiv ~forall alpha .,alpha } ¬ A ≡ A → ⊥ {displaystyle lnot A~equiv ~A o ot } A ∧ B ≡ ∀ α . ( A → B → α ) → α {displaystyle Aland B~equiv ~forall alpha .,(A o B o alpha ) o alpha } A ∨ B ≡ ∀ α . ( A → α ) → ( B → α ) → α {displaystyle Alor B~equiv ~forall alpha .,(A o alpha ) o (B o alpha ) o alpha } ∃ α . M [ α ] ≡ ∀ γ . ( ∀ α . M [ α ] → γ ) → γ {displaystyle exists alpha .,M[alpha ]~equiv ~forall gamma .,(forall alpha .,M[alpha ] o gamma ) o gamma }

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