Расширим это определение, добавив параллельные подстановки:

Можно рассматривать типовые константы как 0-арные конструкторы, т. е. считать, что int задается как int (). Имея определение подстановки, можно счиать, что тип σ является более общим, чем тип σ' и записывать этот факт как . Это отношение выполняется тогда и только тогда, когда существует набор подстановок θ такой, что σ' = σ θ. Например:

Имеет место:

Теорема 4. Каждый типизируемый терм имеет некоторый основной тип, т. е. если Т :: τ, то существует некоторый σ, такой что Т :: σ и для любого σ', если Т :: σ', то .

Доказательство этой теоремы конструктивно: оно дает конкретную процедуру для поиска основного типа. Эта процедура известна как алгоритм ХиндлиМилнера. Все реализации языков программирования типа Haskell включают в себя вариант этого алгоритма. Выражения в них могут быть сопоставлены их основному типу либо отвергнуты как нетипизируемые.

10.3 Сильная нормализация

Справедлива следующая теорема о сильной нормализации:

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

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

36