Что такое тип на самом деле

Разбираемся, что скрывается за словом «тип» и почему типы — это не про память, а про смысл.

Тип — это спецификация: множество допустимых значений вместе с обещанием, какие операции над ними имеют смысл, проверяемая компилятором до запуска программы.

Зачем нам теория типов

Большинство программистов знают типы как «ярлыки»: int, string, bool. Этого хватает, чтобы писать код, но не хватает, чтобы понять, почему один язык ловит ошибку на этапе компиляции, а другой — только в три часа ночи на проде. Теория типов отвечает на вопрос: что такое тип как математический объект и какие гарантии он даёт. Это фундамент, на котором стоят Haskell, Rust, TypeScript, Scala, а также системы доказательств вроде Coq и Lean.

Главная мысль курса проста и радикальна: тип — это не описание битов в памяти, а утверждение о поведении. Когда вы пишете f : Int -> Bool, вы не говорите «f занимает 8 байт». Вы говорите: «дайте мне целое — верну булево, и я обещаю не упасть на полпути». Компилятор превращает это обещание в проверяемую теорему.

Тип как множество значений

Самое интуитивное определение: тип — это множество. Bool — это множество {true, false}. Int (в идеале) — множество всех целых. Значение имеет тип, если принадлежит этому множеству. Запись x : T читается «x имеет тип T» и означает x ∈ T.

Но множество — это ещё не всё. К множеству прилагаются операции, которые имеют смысл. Над Int определено сложение, над Bool — конъюнкция, а складывать булевы или конъюнктить числа — бессмыслица. Тип очерчивает не только «какие значения», но и «что с ними законно делать». Именно поэтому "5" + 3 — ошибка типов в строгом языке: оператор + не определён для пары (String, Int).

Bool  = { true, false }                 -- 2 значения
Unit  = { () }                           -- ровно 1 значение
Void  = { }                              -- 0 значений (тип без обитателей)
Int   = { ..., -2, -1, 0, 1, 2, ... }    -- бесконечное множество

Тип как спецификация и обещание

Более глубокий взгляд: тип — это спецификация интерфейса. Сигнатура length : List a -> Int обещает три вещи: на вход идёт список, на выходе — целое, и функция работает для списка любого элемента a. Это контракт. Компилятор — нотариус, который не даст вам нарушить контракт ни в одной точке программы.

Сравните два мира. В динамическом языке проверка контракта откладывается до выполнения: вызвали length(42) — узнали об ошибке в рантайме, может быть, у клиента. В статически типизированном языке контракт проверяется до запуска: код, нарушающий типы, попросту не скомпилируется. Стоимость ошибки падает с «инцидент на проде» до «красная строка в редакторе».

Маленькая демонстрация: типы ловят бессмыслицу

Python динамичен, но мы можем смоделировать идею типа-как-множества и проверки операции вручную — чтобы увидеть, что именно проверяет система типов.

def add(x, y):
    # имитируем правило типизации оператора +
    if not (isinstance(x, int) and isinstance(y, int)):
        raise TypeError("оператор + определён только для (Int, Int)")
    return x + y

print(add(2, 3))
try:
    add("5", 3)          # нарушение контракта
except TypeError as e:
    print("отвергнуто:", e)

Вывод:

5
отвергнуто: оператор + определён только для (Int, Int)

Настоящая система типов делает такую проверку статически, разом для всей программы, не запуская её. Весь курс — про то, как формализовать и реализовать эту проверку.

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

Когда компилятор «проверяет типы», он строит вывод (derivation): по синтаксическому дереву программы снизу вверх он приписывает каждому подвыражению тип и сверяет их с правилами. Если для корня дерева удалось вывести какой-то тип — программа корректна. Если на каком-то узле правила не сошлись — ошибка типов. Мы научимся читать и реализовывать эти правила в следующих разделах.

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

• «Тип — это представление в памяти». Нет. Int и «индекс массива» могут иметь одно представление, но разные типы, если язык их различает (newtype). Тип — про смысл, а не про байты.
• «Статическая типизация = многословность». Не обязательно: вывод типов (Хиндли — Милнер) позволяет Haskell и OCaml не писать аннотации почти нигде, сохраняя статические гарантии.
• «Типы только мешают». Хороший тип отвергает только программы, которые и так были бы ошибочны. Цена — иногда отвергнутая корректная программа, которую система не смогла доказать.

Итоги

• Тип — это множество значений плюс набор осмысленных операций, проверяемый компилятором.
• Тип — это спецификация и обещание о поведении, а не описание памяти.
• Статическая проверка сдвигает обнаружение ошибки с рантайма на этап компиляции.
• Проверка типов — это построение вывода по правилам; этим мы займёмся весь курс.