Типы как лекарство от парадоксов

Как идея «уровней» убирает порочный круг и почему именно она называется теорией типов.

Теория типов (Рассела) — иерархия уровней, где каждый объект имеет тип, а выражение можно строить только при согласовании уровней: самоприменение запрещено.

Идея уровней

Чтобы убрать парадокс, Рассел в «Principia Mathematica» (1910) предложил расслоить вселенную на уровни. Индивиды — уровень 0. Множества индивидов — уровень 1. Множества множеств индивидов — уровень 2. И так далее. Главное правило: членом множества уровня n+1 могут быть только объекты уровня n. Спросить «содержит ли множество само себя» теперь нельзя: оно и его элементы живут на разных уровнях, выражение x принадлежит x попросту не типизируется.

уровень 0:  индивиды         a, b, c
уровень 1:  множества инд.   {a, b},  {c}
уровень 2:  множества мн-в   { {a,b}, {c} }

x принадлежит y  допустимо ТОЛЬКО если  тип(y) = тип(x) + 1
x принадлежит x  =>  тип(x) = тип(x) + 1  =>  невозможно

Расселово R = { x | x не принадлежит x } больше не строится: само выражение нарушает дисциплину уровней. Болезнь вылечена не запретом «постфактум», а тем, что больной текст невозможно даже записать в системе.

Почему это называется «типом»

Уровень объекта Рассел назвал его типом. Здесь рождается само слово в нашем смысле. Тип — это «слой», к которому принадлежит объект, и операции разрешены только при согласовании слоёв. Спустя полвека эта идея вернулась в программирование: Int и Int -> Int — разные «слои», и применять число как функцию нельзя ровно по той же причине, по которой нельзя x принадлежит x.

Демонстрация: дисциплина уровней на Python

Смоделируем правило «элемент должен быть на уровень ниже коллекции» и увидим, что запрещённое выражение отвергается.

def level_of(obj):
    # уровень = глубина вложенности множеств
    if not isinstance(obj, frozenset):
        return 0
    if len(obj) == 0:
        return 1
    return 1 + max(level_of(e) for e in obj)

def can_contain(container_level, element):
    return level_of(element) == container_level - 1

a = "a"                      # уровень 0
s1 = frozenset({a})          # уровень 1
print("уровень a  :", level_of(a))
print("уровень s1 :", level_of(s1))
print("s1 может содержать a? ", can_contain(level_of(s1), a))
print("s1 может содержать s1?", can_contain(level_of(s1), s1))  # запрещено

Вывод:

уровень a  : 0
уровень s1 : 1
s1 может содержать a?  True
s1 может содержать s1? False

Самовключение отвергается формально — выражение «s1 содержит s1» не проходит проверку уровней. Это та же идея, что отвергнет 5(3) в типизированном языке.

От Рассела к Чёрчу

Теория Рассела была громоздкой. В 1940 году Алонзо Чёрч соединил её с лямбда-исчислением и получил простое типизированное лямбда-исчисление — компактную систему, где типы приписываются функциям и значениям. Именно она — прямой предок систем типов в современных языках, и именно с неё мы начнём формальную часть курса.

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

Лекарство от парадоксов работает структурно: система типов не «ловит» плохое выражение проверкой, а делает его невыводимым — для него нет ни одного правила, которое приписало бы ему тип. Хорошая система типов всегда устроена так, что опасные конструкции (самоприменение, бесконечный спуск) просто не имеют типа.

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

• «Уровни — это про память». Нет, это про логическую согласованность: запрет смешивать объект и коллекцию объектов.
• Считать, что типы только запрещают. Они задают язык допустимых построений; внутри уровней свобода полная.
• Думать, что лечение бесплатно. Иерархия типов отвергает и некоторые безобидные самоссылки; поиск баланса между безопасностью и выразительностью идёт до сих пор.

Итоги

• Расслоение вселенной на уровни (типы) делает самоприменение невыразимым — парадокс исчезает.
• Уровень объекта Рассел назвал его типом; отсюда термин в нашем смысле.
• Чёрч соединил типы с лямбда-исчислением — родилось STLC, предок современных систем типов.
• Опасные конструкции лечатся тем, что становятся невыводимыми, а не запрещёнными постфактум.