Базовые типы

Предположим, что имеется некоторый набор базовых, типов, таких как Bool или Integer. Из них можно конструировать составные типы с помощью конструкторов типов, являющихся, по сути, функциями. Дадим следующее индуктивное определение множества типов, основывающихся на множестве базовых типов С:

Предполагается, что функциональная стрелка —> ассоциативна вправо, т. е. σ —> τ —> ν означает σ —> (τ —> ν).

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

Можно ввести именованные конструкторы произвольной арности. Будем использовать запись Con (α ₁ ,...,α _n ) для применения n -арного конструктора Con к аргументам α _i.

Важным свойством типов является то, что σ —> τ ≠ σ т.е. тип не может совпадать ни с каким своим синтаксически правильным типовым подвыражением. Это исключает возможность применения терма к самому себе.