Элементы теории типов. Простое типизированное λ-исчисление

При обсуждении бестипового λ-исчисления, мы уже столкнулись с “каламбуром”, когда c₀ ≡ fls. Более того, бестиповое λ-исчисление допускает заведомо бессмысленные термы, такие как, например

plus tru c₂

Вообще, удобно кажется ввести некие разумные ограничения на форму термов, такие, что вычисление термов соответствующего вида не заходит в тупик и не приводит к абсурдным результатам.

Бестиповое λ-исчисление с булевскими константами

Рассмотрим язык расширенного λ-исчисления, в котором присутствуют термы-значения true и false, а так же конструкция if ... then ... else. Определим синтаксис:

t ::=     # терм
    x     # переменная
    λx. t # λ-абстракция
    t t   # применение
    if t then t else t # условный оператор

v ::=     # значение
    λx. t # значение-абстракция
    true  # значение-истина
    false # значение-ложь

Определим операционную семантику (с малым шагом)

   t₁ -> t₁'
---------------
t₁ t₂ -> t₁' t₂

   t₂ -> t₂'
---------------
v₁ t₂ -> v₁ t₂'

       t₀ -> t₀'
--------------------------
  if t₀ then t₁ else t₂
 -> if t₀' then t₁ else t₂

       t₁ -> t₁'
--------------------------
  if v₀ then t₁ else t₂
 -> if v₀ then t₁' else t₂

       t₂ -> t₂'
--------------------------
  if v₀ then v₁ else t₂
 -> if v₀ then v₁ else t₂'

if true then v₁ else v₂ -> v₁

if false then v₁ else v₂ -> v₂

(λx. t) v -> [x -> v]t

Эти правила определяют порядок вычислений. Действительно, пока возможно, вычисляется левый терм. Когда левый терм пришёл к значению, вычисляется следующий в порядке слева направо терм. Если все термы операции пришли к значению, производится применение. Собственно первые 5 правил только сопоставляют одни термы другим, определяя порядок вычисления, а операционными являются последние три.

Отдельно отметим, что такая операционная семантика соответствует следующей денотационной с бестиповым λ-исчислением при вычислении порядке вызова по значению:

# термы
[[x]] = x # переменная
[[λx. t]] = λx. [[t]]
[[t₁ t₂]] = [[t₁]] [[t₂]]
[[if t₁ then t₂ else t₃]] = ifThenElse [[t₁]] [[t₂]] [[t₃]]

# значения
[[true]] = tru
[[false]] = fls

Теперь, мы бы хотели модифицировать это исчисление таким образом, чтобы исключить возможность бессмысленных термов, например, таких: if (λx. x) then true else false, не производя самого вычисления. Под “бессмысленным” здесь будем понимать термы, которые не являются значениями, но при этом заходят в “тупик”, т.е. не могут быть далее редуцированы в рамках определённой операционной семантики.

Правила типизации для булевских выражений

Собственно, пример выше выглядит достаточно тривиально: первый член выражения if должен быть булевским значением, чтобы выражение имело смысл. Для введения подобных ограничений вводится отношение типизации.

Отношение типизации, записываемое в виде t : T или t ∈ T, читается как “терм t имеет тип T” или “терм t принадлежит типу T”, и определяется набором правил, присваивающих термам типы. Эти правила называются правилами вывода типов, или правилами типизации.

Отношение типизации
Более формально, отношение типизации – это наименьшее бинарное отношение между термами и типами, удовлетворяющее всем правилам типизации. Терм t называется типизируемым или корректно типизированным, если существует тип T, такой, что t : T.

Введём новые синтаксические формы:

T ::=       # Типы
    Bool    # Булевские значения

и правила типизации

true : Bool

false : Bool

t₁ : Bool, t₂ : T, t₃ : T
--------------------------
if t₁ then t₂ else t₃ : T

Поскольку мы хотим в результате присвоить тип каждому терму, здесь нам приходится ввести дополнительное требование, чтобы второй и третий термы в выражении if имели одинаковый тип (и соответственно тогда мы можем присвоить однозначный тип всему выражению if не производя вычисления). Следует заметить, что это ограничение запрещает некоторые корректные программы, например, if false then (λx. true) else true – понятно, что результатом этого терма всегда будет true. Однако в общем случае эта задача неразрешима, т.е. термы вида if <сложное вычисление> then (λx. true) else true типизировать, не вычисляя <сложное вычисление> явно не получится.

Корректно определённое отношение типизации должно определять ровно один тип для каждого терма (чтобы избежать неоднозначности). Так же корректно определённое отношение типизации называют безопасной или корректной системой типов.

Корректность системы типов строго доказывается через доказательство свойств продвижения и сохранения.

Продвижение
Корректно типизированный терм не может быть тупиковым (т.е. это либо значение, либо возможен шаг вычисления)
Сохранение
Если корректно типизированный терм проделывает шаг вычисления, получается также корректно типизированный терм.

Обычно эти свойства доказывают при помощи структурной индукции над правилами вывода типов и вычисления. В этом изложении опустим доказательства1, но отметим, что введённая система типов для булевских выражений и оператора if является корректной (безопасной).

Правила типизации функций (λ-абстракций)

Мы, однако, по-прежнему не можем типизировать λ-абстракции. Чтобы их типизировать, нам нужно ввести тип, описывающий функции. Допустим, мы введём тип F для всех λ-абстракций, λx. t : F. Тогда мы сможем типизировать конструкции вида λx. x : F или if true then (λx. true) else (λx.λy.y) : F. Однако, с применением возникают сложности. Например, во втором примере, применение выражения к переменной в одной ветви if даст булево значение, а в другом случае – функцию.

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

Для сбора этой информации, мы заменим тип F на семейство типов вида T₁ -> T₂, каждый из которых описывает функции, принимающие аргументы типа T₁ и возвращающие результаты типа T₂.

Тогда синтаксис для типов примет вид:

T ::=       # Типы
    Bool    # Булевские значения
    T -> T  # Функции

Будем называть оператор -> конструктором типа функции. Условимся, что он право-ассоциативен, т.е. выражение T₁ -> T₂ -> T₃ следует читать как T₁ -> (T₂ -> T₃)

Чтобы определить тип λ-абстракции вида λx. t, надо понять, что случится, когда эта абстракция будет применена к какому-либо аргументу. Как определить, аргументов какого типа следует ожидать? Существуют два варианта:

  • Явная типизация. Пометить λ-абстракцию типом ожидаемого аргумента
  • Неявная типизация. Анализировать тело λ-абстракции и из контекста пытаться определить тип аргумента.

Для простоты, пока выберем первый вариант, добавив аннотацию типа аргумента в синтаксис λ-абстракции.

Если известен тип аргумента, тип результата получается подстановкой соответствующего типа для переменной в правило типизации для тела функции. Эту идею можно выразить следующим формальным правилом:

  x : T₁ |- t₂ : T₂
---------------------
λx: T₁. t₂ : T₁ -> T₂

(здесь |- следует читать как логическое следствие, “из левого утверждение выводится правое”)

Поскольку термы могут содержать вложенные λ-абстракции, предположений вида x : T₁ может быть несколько. Будем обозначать множество таких предположений символом Γ. В данном случае Γ – это множество предположений о типах свободных переменных.

Формально, контекст типизации Γ представляет собой последовательность переменных и их типов, и может быть расширен в стандартной нотации при помощи оператора “запятая”. Пустой контекст для краткости будем просто опускать, имея ввиду, что в отсутствие контекста, подразумевается вывод из пустого множества предположений.

Для избежания конфликтов имён, потребуем, чтобы новые переменные, добавляемые к Γ имели имена, не присутствующие ещё в Γ. Тогда Γ можно представлять как функцию, переводящую имена переменных в их типы. Следуя этому представлению, множество переменных, присутствующих в Γ обозначим как dom(Γ).

Правило типизации для абстракции в общем виде тогда:

   Γ, x : T₁ |- t₂ : T₂
--------------------------
Γ |- λx: T₁. t₂ : T₁ -> T₂

Правило типизации переменных тогда тривиально

x : T ∈ Γ
----------
Γ |- x : T

т.е. тип переменной – это тип, который она имеет согласно Γ.

Наконец, мы можем сформулировать правило типизации для применений:

Γ |- t₁ : T₁₁ -> T₁₂ ; Γ |- t₂ : T₁₁
------------------------------------
          Γ |- t₁ t₂ : T₁₂

Простое типизированное λ-исчисление с булевскими значениями

Теперь целиком опишем синтаксис, операционную семантику и систему типов для простого типизированного λ-исчисления, расширенную булевскими значениями.

Синтаксис:

t ::=       # терм
    x       # переменная
    λx:T. t # λ-абстракция
    t t     # применение
    if t then t else t # условный оператор

v ::=       # значение
    λx:T. t # значение-абстракция
    true    # значение-истина
    false   # значение-ложь

T ::=       # Типы
    Bool    # Булевское значение
    T -> T  # Абстракция (функция)

Γ ::=       # Контексты
    ∅       # Пустой контекст
    Γ, x: T # Связывание переменной

Операционная семантика вычисления полностью повторяет ранее введённую, за исключением добавления типа переменной в последнем правиле:

   t₁ -> t₁'
---------------
t₁ t₂ -> t₁' t₂

   t₂ -> t₂'
---------------
v₁ t₂ -> v₁ t₂'

       t₀ -> t₀'
--------------------------
  if t₀ then t₁ else t₂
 -> if t₀' then t₁ else t₂

       t₁ -> t₁'
--------------------------
  if v₀ then t₁ else t₂
 -> if v₀ then t₁' else t₂

       t₂ -> t₂'
--------------------------
  if v₀ then v₁ else t₂
 -> if v₀ then v₁ else t₂'

if true then v₁ else v₂ -> v₁

if false then v₁ else v₂ -> v₂

(λx:T. t) v -> [x -> v]t

Наконец, правила типизации:

true : Bool

false : Bool

Γ |- t₁ : Bool; Γ |- t₂ : T; Γ |- t₃ : T
--------------------------------------
   Γ |- if t₁ then t₂ else t₃ : T

x : T ∈ Γ
----------
Γ |- x : T

   Γ, x : T₁ |- t₂ : T₂
--------------------------
Γ |- λx: T₁. t₂ : T₁ -> T₂

Γ |- t₁ : T₁₁ -> T₁₂ ; Γ |- t₂ : T₁₁
-----------------------------------
          Γ |- t₁ t₂ : T₁₂

Отметим, что в правиле для выражения if, мы должны также ввести контекст Γ, поскольку это выражение может встречаться в теле λ-абстракций.

Из правил типизации можно конструировать деревья вывода типа – формальные индуктивные построения, показывающие, что терм имеет корректный тип. Например, покажем, что терм (λx:Bool. x) true имеет тип Bool в пустом контексте:

  x : Bool ∈ {x : Bool}
  ----------------------
   x : Bool |- x : Bool
----------------------------
(λx:Bool. x) : Bool -> Bool ; true : Bool
----------------------------------------------------
   Γ |- (λx:Bool. x) true : Bool

Отдельно следует отметить, что чистое простое типизированное λ-исчисление – не содержащее значений кроме абстракций – является вырожденным, т.е. не содержит корректно типизированных термов.

Упражнение Покажите (построением деревьев вывода), что следующие термы имеют заялвенные типы:

  1. f: Bool -> Bool |- f (if false then true else false) : Bool
  2. f: Bool -> Bool |- λx:Bool. f (if x then false else x) : Bool -> Bool

Упражнение Найдите контекст Γ, в котором терм f x y имеет тип Bool. Можно ли описать множество всех таких контекстов?

Соответствие Карри-Говарда

Конструктору типов -> соответствуют два вида правил:

  1. Правило введения, которое показывает, как элементы типа могут создаваться:

       Γ, x : T₁ |- t₂ : T₂
--------------------------
Γ |- λx: T₁. t₂ : T₁ -> T₂

  2. Правило устранения, которое показывает, как элементы типа могут использоваться:

    Γ |- t₁ : T₁₁ -> T₁₂ ; Γ |- t₂ : T₁₁
-----------------------------------
          Γ |- t₁ t₂ : T₁₂

Такая ситуация характерна для любых конструкторов типов.

Терминология “правило введения/устранения” происходит из соответствия между теорией типов и формальной логикой, известного как соответствие или изоморфизм Карри-Говарда. В двух словах, в конструктивных логиках (не включающих закон исключённого третьего в аксиоматику, т.е. по сути запрещающих доказательства от противного), доказательство утверждения P состоит в демонстрации конкретного свидетельства в пользу P. Карри и Говард заметили, что такое свидетельство эквивалентно некоторому алгоритму вычисления значения из P. Собственно, само соответствие проводится между понятием утверждений в формальной логике и понятием типов в теории типов. Например, вот несколько примеров эквивалентности:

Логика Теория типов
утверждение P ⊃ Q тип P -> Q
утверждение P ∧ Q тип P×Q
доказательство P терм t : P
утверждение P доказуемо существуют термы типа P

В этом смысле, терм в простом типизированном λ-исчислении является доказательством соответствующего его типу логического утверждения. Вычисление (редукция) соответствует упрощению доказательств методом устранения сечений.

Прелесть соответствия Карри-Говарда в том, что соответствие не ограничено одной логикой и одной системой типов. Так, более “продвинутые” системы типов соответствуют более “продвинутым” логическим системам, в частности System F, являющаяся теоретическим основанием для системы типов Haskell, соответствует конструктивной логике второго порядка.

Соответствие Карри-Говарда неоднократно использовалось для переноса результатов из формальной логики в теорию типов и наоборот.

Стирание типов

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

Определим функцию стирания типов для типизированного терма:

erase(x) = x
erase(λx:T. t) = λx. erase(t)
erase(t₁ t₂) = erase(t₁) erase(t₂)

Собственно, если внимательно присмотреться, то функция erase здесь играет роль денотационных скобок erase(x) ≈ [[x]].

Разумеется, мы ожидаем, что поведение программы до и после стирания типов не изменяется. Для приведённого выше случая это тривиально доказывается индукцией по правилам операционной семантики, но в более интересных языках и с более интересными компиляторами, важность этой эквивалентности возрастает. По сути, мы утверждаем, что семантика, выраженная на “высокоуровневом” языке совпадает с фактически используемой “низкоуровневой” стратегией вычисления.

  1. См. Пирс, Типы в языках программирования, раздел 8.3 (с. 97)↩︎