10.1 Типизированное лямбда-исчисление
Модифицируем лямбда-исчисление введя в него понятие типа. Каждый лям- бда-терм должен иметь тип, причем терм S можно применить к терму Т в комбинации S Т, если их типы правильно соотносятся друг с другом, т.е. S имеет тип функции σ —> τ и Т имеет тип σ. В результате, S Т, имеет тип τ. Это свойство называется сильной типизацией. Приведение типов не допускается.
Будем использовать запись вида Т :: σ для утверждения «Т имеет тип σ».
10.1.1 Базовые типы
Предположим, что имеется некоторый набор базовых, типов, таких как Bool или Integer. Из них можно конструировать составные типы с помощью конструкторов типов, являющихся, по сути, функциями. Дадим следующее индук-
тивное определение множества типов
, основывающихся на множестве базовых типов С:
Предполагается, что функциональная стрелка —> ассоциативна вправо, т. е. σ —>
τ—> νозначаетσ—> (τ—> ν).
Можно расширить систему типов двумя способами. Во-первых, можно ввеси понятие типовых, переменных, являющихся средством для реализации полиморфизма. Во-вторых, можно ввести дополнительные конструкторы типов, помимо функциональной стрелки, например конструктор х для типа пары значений. В этом случае необходимо добавить правило:
Можно ввести именованные конструкторы произвольной арности. Будем использовать запись Con ( α1 , ... , αn ) для применения n-арного конструктора Con к аргументам αi .
Важным свойством типов является то, что σ —> τ ≠ σ т.е. тип не может совпа-
32
дать ни с каким своим синтаксически правильным типовым подвыражением. Это исключает возможность применения терма к самому себе.
10.1.2 Типизации по Черчу и Карри
Существуют два основных подхода к определению типизированного лям- бда-исчисления. Первый подход, принадлежащий Черчу это явная типизация. Каждому терму сопоставляется единственный тип. Это означает, что в процессе конструирования термов, нетипизированные термы модифицируются с помощью дополнительной характеристики - типа. Для констант этот тип задан заранее, но переменные могут иметь любой тип. Правила корректного формирования термов выглядят следующим образом:
Однако мы будем использовать для типизации подход Карри, который является неявным. Термы могут иметь или не иметь типа, и если терм имеет тип, то он может быть не единственным. Например, функция идентичности λх. х может иметь любой тип вида σ —> σ. Такой подход более предпочтителен, поскольку, во-первых, он соответствует используемому в языках типа Haskell понятию полиморфизма, а во-вторых, позволяет не задавать типы явным образом.
Определим понятие типизируемости по отношению к контексту, т. е. конечному набору предположений о типах переменных. Будем записывать:
чтобы обозначить, что «в контексте ? терм Т может иметь тип σ». Будем употреблять запись 
или просто Т :: σ, если суждение о типизации выполняется в пустом контексте. Элементы контекста ? имеют вид ν :: σ, т. е. они представляют собой предположения о типах переменных. Будем предполагать, что в ? нет противоречивых предположений.
33