Зачем типизировать лямбда-исчисление

Переход от «всё можно» к «можно только осмысленное»: что мы выигрываем и что теряем, добавляя типы.

Простое типизированное лямбда-исчисление (STLC) — лямбда-исчисление, где каждому терму приписывается тип, а применять можно только функцию к аргументу подходящего типа.

Болезни нетипизированного мира

Нетипизированное лямбда-исчисление Тьюринг-полно — и в этом его проблема для рассуждений. Два симптома. Во-первых, в нём есть бессмысленные термы: ничто не мешает применить число Чёрча к числу или взять «голову» там, где её нет, — структура есть, смысла нет. Во-вторых, есть незавершающиеся термы вроде (\x. x x)(\x. x x), которые крутятся вечно. Для модели вычислений это норма, но для языка, где мы хотим гарантий, — беда.

Что добавляют типы

STLC вводит типы и одно ключевое ограничение на аппликацию: применять f a можно, только если f имеет тип-функцию A -> B, а a имеет тип A; результат тогда типа B. Самоприменение x x перестаёт типизироваться: чтобы x был и функцией A -> B, и её аргументом A одновременно, нужен A = A -> B — бесконечный тип, которого в STLC нет.

Типы:  T ::= Base            -- базовый тип (Int, Bool, ...)
          | T -> T           -- тип функции

Аппликация f a типизируется, ТОЛЬКО если
   f : A -> B   и   a : A    тогда   f a : B

Великая теорема: сильная нормализация

Плата за типы огромна по последствиям: каждый типизируемый терм STLC завершается (теорема о сильной нормализации). Незавершающихся программ в STLC попросту нет. Это прекрасно для доказательств и ужасно для «настоящего» программирования: STLC не Тьюринг-полно, на нём нельзя написать произвольный цикл. Реальные языки возвращают мощь, добавляя рекурсию отдельной конструкцией (с потерей гарантии завершаемости).

Демонстрация: какие термы «выживают»

Смоделируем фильтр STLC грубо: пометим, типизируем ли мы терм, на примере самоприменения. Полноценный чекер построим в разделе 4 далее; здесь — интуиция «почему x x вне закона».

# чтобы x : A -> B применялось к x : A, нужно A = (A -> B)
# это уравнение не имеет конечного решения -- значит, типа нет
def can_self_apply(A, arrow_from, arrow_to):
    # пытаемся: A должно равняться (A -> B); смоделируем как строку
    needed = "(" + A + " -> " + arrow_to + ")"
    return A == needed       # никогда не совпадёт для конечного A

print("x x типизируется?", can_self_apply("a", "a", "b"))
print("вывод: для x x нужен бесконечный тип a = (a -> b) -- его в STLC нет")

Вывод:

x x типизируется? False
вывод: для x x нужен бесконечный тип a = (a -> b) -- его в STLC нет

Как работает под капотом

STLC добавляет к синтаксису термов синтаксис типов и систему правил вывода (раздел 4, урок про правила). Каждое правило говорит, при каких типах подвыражений терм получает свой тип. Терм «существует» в STLC, только если для него можно построить дерево вывода. Бессмысленные и незавершающиеся термы такого дерева не имеют — они отсеиваются автоматически.

Частые ошибки

• Думать, что типы «ничего не запрещают полезного». STLC теряет Тьюринг-полноту — это цена сильной нормализации. Баланс мощи и гарантий — сквозная тема курса.
• Считать самоприменение «просто странным». Оно строго невыводимо: требует бесконечного типа.
• Ожидать рекурсию «бесплатно». В чистом STLC её нет; реальные языки добавляют её отдельной конструкцией fix/let rec.

Итоги

• Нетипизированное исчисление допускает бессмысленные и незавершающиеся термы.
• STLC ограничивает аппликацию: функция A -> B применяется к аргументу A.
• Самоприменение невыводимо: требует бесконечного типа.
• Каждый типизируемый терм STLC завершается (сильная нормализация) — ценой Тьюринг-полноты.