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

В бестиповом λ-исчислении возможны каламбуры c₀ ≡ fls.
допускает заведомо бессмысленные термы, например plus tru c₂
удобно ввести разумные ограничения на форму термов, такие, что вычисление не заходит в тупик и не приводит к абсурдным результатам.

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

Расширим λ-исчисление термами-значениями true и false, и конструкцией if ... then ... else.

Cинтаксис

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 false then (λx. true) else true
в общем случае термы вида if <...> then (λx. true) else true, не вычисляя <...>, не получится типизировать

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

Корректность – это продвижение и сохранение

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

Обычно доказывают при помощи структурной индукции над правилами вывода типов и вычисления.
Опустим доказательства (См. Пирс, раздел 8.3, с. 97)
Отметим, что наша система типов – корректная (безопасная)

Правила типизации λ-абстракций

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

нужно знать не только, что это функция, но и то, какой у неё тип результата
для гарантий правильного поведения, нужно знать тип аргумента, ожидаемый функцией
заменим тип F на семейство типов T₁ → T₂
T₁ → T₂ описывает функции, аргумент типа T₁ и результат типа T₂

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

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

оператор → – конструктор типа функции
Условимся, что он право-ассоциативен, т.е. T₁ → T₂ → T₃ \(\equiv\) T₁ → (T₂ → 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₁₂

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

  x : Bool ∈ {x : Bool}
  ―――――――――――――――――――――
   x : Bool ⊢ x : Bool
――――――――――――――――――――――――――
(λx:Bool. x) : Bool → Bool ; true : Bool
―――――――――――――――――――――――――――――――――――――――――
   Γ ⊢ (λx:Bool. x) true : Bool

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

Упражнение Покажите (построением деревьев вывода), что следующие термы имеют заявленные типы:
```
f: Bool → Bool ⊢ f (if false then true else false) : Bool
```
```
f: Bool → Bool ⊢ λx:Bool. f (if x then false else x) : Bool → Bool
```
Упражнение Найдите контекст Γ, в котором терм f x y имеет тип Bool. Можно ли описать множество всех таких контекстов?

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

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

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

   Γ, x : T₁ ⊢ t₂ : T₂
――――――――――――――――――――――――
Γ ⊢ λx: T₁. t₂ : T₁ → T₂

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

Γ ⊢ 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]].
мы ожидаем, что поведение программы до и после стирания типов не изменяется.
Здесь это тривиально доказывается индукцией по правилам операционной семантики
в более интересных (сложных) языках, важность этой эквивалентности возрастает
семантика, выраженная на “высокоуровневом” языке совпадает с фактически используемой “низкоуровневой” стратегией вычисления.