Теория языков программирования

Алгебраические типы данных

Ошибка на миллиард долларов

В 1965 году Тони Хоар изобрёл null-ссылку для ALGOL W. В 2009 году он публично назвал это своей самой большой ошибкой: null-разыменование стало причиной бесчисленных крашей и уязвимостей. Алгебраические типы - ответ функциональных языков: `Maybe`/`Option` в Haskell и ML появились в 1970-80-х и полностью исключили null из системы типов.

В 2013 году баг в коде Apple (`goto fail`) привёл к тому, что SSL-верификация сертификата всегда возвращала успех. Причина - обычный `if` без match, где один вариант ошибки был пропущен. Exhaustiveness checking сделал бы этот баг невозможным на уровне компиляции.

  • **Rust std::Result** - возвращаемые ошибки невозможно проигнорировать; компилятор предупреждает о неиспользованном Result
  • **TypeScript discriminated unions** - React-компоненты для разных состояний (loading / error / data) без null-проверок
  • **Haskell Maybe** - отсутствие null в языке; все «необязательные» значения явно типизированы

Sum Types: значение - это одно из

В 1965 году Тони Хоар добавил в ALGOL W значение `null` - и назвал это своей «ошибкой на миллиард долларов». Null существует потому, что языки не могли выразить идею «значения нет» на уровне типов. **Sum types** решают эту проблему: тип `Maybe<T>` имеет ровно два варианта - либо `Nothing` (значения нет), либо `Just(x)` (значение есть). Третьего не дано.

Sum type (тип-сумма) означает, что значение является **одним из** нескольких вариантов. Количество возможных значений суммируется: `|A + B| = |A| + |B|`. Для `Maybe<Bool>`: `|Nothing| + |Just(Bool)| = 1 + 2 = 3` возможных значения.

**Ключевая идея:** sum type делает невозможные состояния невыразимыми. Функция, возвращающая `Result<User, DbError>`, не может «забыть» обработать ошибку - компилятор не даст обратиться к `User` без проверки варианта.

Тип `data Color = Red | Green | Blue` - сколько возможных значений у этого sum type?

Product Types: значение - это всё сразу

Структура `Point { x: f64, y: f64 }` содержит **и** поле x **и** поле y одновременно. Это product type - количество возможных значений перемножается: `|Point| = |f64| × |f64|`. Кортежи, структуры и записи - всё это product types.

ТипЛогикаКоличество значенийПример
Sum (union)A ИЛИ B|A| + |B|Ok(T) | Err(E)
Product (struct)A И B|A| × |B|{ name: String, age: u8 }
Unit1 вариант1() в Rust, void
Never/Bottom0 вариантов0never в TypeScript

Комбинируя sum и product types, можно точно описать допустимые состояния. Классический пример: состояние сетевого соединения - `Connected { socket: Socket, timeout: Duration }` или `Disconnected { reason: CloseReason }`. Попасть в `Connected` без `socket` структурно невозможно.

Тип `{ ok: boolean; value: string }` - это:

Pattern Matching: деструктуризация по форме

Pattern matching - это не «switch с синтаксическим сахаром». Это структурная деструктуризация: компилятор проверяет форму значения и одновременно извлекает поля. Для sum type обязательно покрыть **все** варианты - иначе ошибка компиляции.

**Отличие от switch:** в switch проверяется равенство значений. В pattern matching проверяется структура - вариант конструктора, вложенные поля, диапазоны. Это позволяет деструктурировать вложенные типы в одном выражении.

Чем pattern matching принципиально отличается от обычного switch/case?

Exhaustiveness: компилятор как страховка

Exhaustiveness checking - проверка того, что match покрывает **все** варианты sum type. Когда в будущем добавляется новый вариант, компилятор укажет на все места, где нужно обработать его. Без этого - тихий баг в рантайме.

**Антипаттерн:** `default:` в switch уничтожает exhaustiveness - новые варианты молча попадут в default-ветку. Предпочтительнее явно перечислить все варианты или использовать `assertNever`.

Sum types - это просто enum с числовыми значениями, как в C.

Sum types в ML/Rust/Haskell несут данные в каждом варианте и требуют pattern matching для извлечения. C enum - просто именованные целые числа без проверки типов вложенных данных.

В C `enum Status { OK = 0, ERR = 1 }` не несёт данных и не даёт exhaustiveness checking. В Rust `enum Result<T,E> { Ok(T), Err(E) }` содержит типизированные данные в каждом варианте.

К enum добавили новый вариант. Что произойдёт в языке с exhaustiveness checking?

Алгебраические типы данных

  • **Sum type (OR):** значение - одно из вариантов; |A+B| = |A|+|B|; устраняет null через Maybe/Option/Result
  • **Product type (AND):** значение содержит все поля одновременно; |A×B| = |A|×|B|; структуры и кортежи
  • **Pattern matching:** структурная деструктуризация - проверяет форму и извлекает поля в одном выражении
  • **Exhaustiveness:** компилятор требует покрыть все варианты; добавление нового варианта - это ошибка компиляции, не рантайм-сюрприз

Связанные темы

Алгебраические типы - основа для более продвинутых концепций типовой системы.

  • Дженерики и параметрический полиморфизм — Maybe<T> и Result<T,E> - sum types с type parameters
  • Типы высшего порядка — Functor/Monad - абстракции над контейнерными sum types

Вопросы для размышления

  • В каких ситуациях product type с булевым флагом `{ data: T; isError: boolean }` хуже sum type `Ok(T) | Err(E)` с точки зрения корректности?
  • Как exhaustiveness checking меняет процесс рефакторинга - добавления нового варианта в существующий sum type?
  • Почему в языках с null (Java, C#) до сих пор не исчезли NullPointerException, несмотря на аннотации `@Nullable` / `?`?

Связанные уроки

  • plt-06-lambda-calculus — ADTs arise naturally from the lambda calculus; Church encodings show product and sum types as lambda terms
  • plt-08-generics — Generic ADTs (Maybe<T>, Result<T, E>) combine algebraic types with parametric polymorphism
  • plt-11-typeclasses — Typeclasses like Functor and Foldable are typically defined over ADTs; the concepts build on each other
  • plt-03-static-vs-dynamic — ADTs shine in static languages - context helps appreciate why exhaustive pattern matching matters
  • dm-01
Алгебраические типы данных

0

1

Войти