Типы как спецификация и предотвращение ошибок

Почему хороший тип сужает множество возможных программ до множества правильных.

Выразительность системы типов — мера того, сколько ошибочных программ она способна отвергнуть, не отвергая при этом полезных.

Тип как сужение пространства программ

Представьте все мыслимые тексты на языке. Подавляющее большинство — мусор. Синтаксис отсекает то, что нельзя даже разобрать. Система типов отсекает следующий слой: то, что разбирается, но не имеет смысла — true + 1, вызов числа как функции, чтение поля у списка. Чем выразительнее типы, тем уже воронка, тем больше гарантий «если скомпилировалось — скорее всего работает».

Классический лозунг сообщества Haskell: «make illegal states unrepresentable» — сделай недопустимые состояния невыразимыми. Если тип описывает только корректные значения, то целый класс багов становится физически невозможным: не «мы поймали ошибку», а «ошибку нельзя написать».

Слабая спецификация против сильной

Сравните две сигнатуры функции «взять первый элемент»:

head : List a -> a          -- врёт: на пустом списке элемента нет
head : NonEmptyList a -> a  -- честно: вход гарантированно непуст

Первая сигнатура лжёт: на пустом списке функция обязана либо упасть, либо вернуть несуществующее значение. Вторая переносит требование «непустой» в тип аргумента — и тогда вызвать head на пустом списке невозможно по построению. Тип стал спецификацией, а не украшением.

Ещё пример — деление. div : Int -> Int -> Int скрывает, что делитель не может быть нулём. Более честный тип потребовал бы NonZero на втором аргументе. Языки с зависимыми типами умеют выражать и это.

Демонстрация: тип Option вместо «может быть null»

Самый знаменитый «баг на миллиард долларов» — null. Тип Option (он же Maybe) превращает «значения может не быть» из невидимой ловушки в видимую часть сигнатуры. Смоделируем на Python.

def safe_div(a, b):
    # тип результата: Option[Int] = ("some", v) | ("none",)
    if b == 0:
        return ("none",)
    return ("some", a // b)

def show(opt):
    if opt[0] == "some":
        return "результат = " + str(opt[1])
    return "деления нет (none)"

print(show(safe_div(10, 2)))
print(show(safe_div(10, 0)))

Вывод:

результат = 5
деления нет (none)

Сигнатура safe_div : Int -> Int -> Option Int заставляет вызывающего обработать оба случая. Компилятор языка с алгебраическими типами не даст «забыть» ветку none — отсюда исчезает целый класс NPE.

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

Когда мы обогащаем тип (например, NonEmptyList вместо List), мы добавляем в систему дополнительные правила построения и разбора значений. Конструктор непустого списка требует хотя бы один элемент, поэтому никакая последовательность правил не построит пустое значение этого типа. Невозможность бага вытекает не из договорённости, а из того, что в выводе нет правила, дающего «плохое» значение.

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

Перенос проверок в рантайм при наличии типового решения. Если можно выразить инвариант в типе — выражайте; рантайм-проверка повторяет работу компилятора.
Слишком сильные типы. Бесконечно точная спецификация дороже в написании и может отвергнуть полезный код. Инженерное искусство — баланс между гарантиями и удобством.
Путать «скомпилировалось» с «правильно». Типы исключают класс ошибок, но не логические баги внутри допустимого типа. Тип Int -> Int не отличит сложение от вычитания.

Итоги

Тип сужает множество программ, отсекая бессмысленные ещё до запуска.
Сильная спецификация переносит инварианты («непустой», «не ноль», «может отсутствовать») в тип.
Option/Maybe делает отсутствие значения видимым и обязательным к обработке.
Выразительность — это баланс: больше гарантий ценой большего труда.