Типизированные λ-исчисления

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

Простейшая такая система — просто типизированное λ-исчисление (λ→\lambda^{\to}). Каждый терм в ней получает тип, а сами типы строятся из атомарных α\alpha единственной конструкцией — стрелкой:

τ  ::=  α  ∣  τ\displaystyle \tau \;\mathrel{\text{::=}}\; \alpha \;\mid\; \tau →τ\displaystyle \to \tau
(1.37)

Три правила вывода — по одному на конструкцию терма:

x:τ∈ΓΓ⊢x:τΓ,  x:σ⊢M:τΓ⊢λx. M:σ→τΓ⊢M:σ→τΓ⊢N:σΓ⊢M N:τ\frac{x{:}\tau \in \Gamma}{\Gamma \vdash x : \tau} \qquad \frac{\Gamma,\; x{:}\sigma \vdash M : \tau}{\Gamma \vdash \lambda x.\,M : \sigma \to \tau} \qquad \frac{\Gamma \vdash M : \sigma \to \tau \quad \Gamma \vdash N : \sigma}{\Gamma \vdash M\,N : \tau}
(1.38)

Слева направо: переменная берёт свой тип из контекста Γ\Gamma; абстракция — если в предположении x:σx{:}\sigma тело MM имеет тип τ\tau, то λx. M\lambda x.\,M — функция типа σ\sigma →τ\to\tau; аппликация — функцию σ\sigma →τ\to\tau можно применить только к аргументу типа σ\sigma, и результат получает тип τ\tau.

Есть два важных свойства: первое — сильная нормализация: всякий типизируемый терм имеет НФ, и любой порядок редукции её достигает — как следствие, Ω\Omega и Y\mathrm{Y} нетипизируемы, а язык не полон по Тьюрингу; второе — subject reduction: тип сохраняется при редукции — «вычисление не портит тип».

А что насчёт полиморфизма? Причём по типам. В λ→\lambda^{\to} его нет: тождественная функция λx:α. x\lambda x{:}\alpha.\,x привязана к одному конкретному типу α\alpha, и для каждого нового типа её приходится писать заново. Жирар и Рейнольдс устранили это ограничение, разрешив термам абстрагироваться не только по значениям, но и по самим типам, — получилась System F, для которой справедливо следующее:

id\displaystyle \mathrm{id} =Λα. λx:α. x  :  ∀α. α\displaystyle = \Lambda\alpha.\,\lambda x{:}\alpha.\,x \;:\; \forall\alpha.\,\alpha →α\displaystyle \to\alpha

Здесь Λα\Lambda\alpha — абстракция по типу: id\mathrm{id} принимает сначала тип α\alpha, затем значение xx этого типа и возвращает его же. Тип ∀α. α\forall\alpha.\,\alpha →α\to\alpha читается «для любого типа α\alpha — функция из α\alpha в α\alpha»: одна и та же id\mathrm{id} применима к числу, булеву значению, функции — полиморфизм стал частью самого исчисления.

Вывод типов в полной System F неразрешим, поэтому Haskell использует разрешимый фрагмент — систему Хиндли — Милнера (алгоритм W), где все типы выводятся без аннотаций; ей посвящён следующий раздел.