«Алгебраические» — буквально: типы можно складывать и умножать, и они образуют полукольцо. Произведение — это «И», сумма — «ИЛИ». Из этих двух операций собираются структуры, в которых недопустимые состояния просто нельзя выразить. Здесь алгебра из главы I встречается с функциональным программированием из главы VI.
Тип — это множество возможных значений. У Bool их два, у единичного типа — одно, у пустого — ни одного. Раз так, типы можно складывать и умножать, как числа, а у составного типа — считать число обитателей. Эта «арифметика типов» и дала название: алгебраические типы данных.
Польза двойная. Во-первых, это прямой мост из главы об алгебре: типы образуют ту же структуру — полукольцо. Во-вторых, считая значения, инженер видит, какие состояния вообще возможны, — и может сделать недопустимые невыразимыми.
Кортеж, запись, структура: A и B одновременно. Число значений перемножается: $|A\times B| = |A|\cdot|B|$.
Тегированное объединение: A или B. Число значений складывается: $|A + B| = |A| + |B|$. Это Maybe, Either, Result.
В типизированных языках это пишется прямо:
Единицы и поглощение — как в арифметике:
$A\times 1 \cong A,\qquad A + 0 \cong A,\qquad A\times 0 \cong 0$
И дистрибутивность — умножение раскрывается над суммой:
$A\times(B + C)\;\cong\;A\times B \,+\, A\times C$
Где $0$ — пустой тип (значений нет), $1$ — единичный (одно значение, как () или :ok). Изоморфизм $\cong$ означает «одинаковое число значений и взаимно-обратные преобразования». Посчитаем обитателей:
Что это даёт практически: изоморфные типы взаимозаменяемы. Например, $\mathrm{Maybe}\,a \cong 1 + a$ — то же, что «либо ничего, либо значение». А распределительный закон подсказывает безопасные рефакторинги представления данных, не меняющие множество допустимых значений.
Три булевых поля дают $2\times2\times2 = 8$ комбинаций, из которых осмысленны три. Сумма-тип оставляет ровно допустимые состояния — остальные просто не существуют как значения. А исчерпывающий разбор (pattern matching) заставляет обработать каждый вариант: компилятор или линтер укажет на пропуск. Это и есть мост к главе о математически корректных программах — частный случай тотальности.
В Elixir статических сумм-типов нет, но идиома та же: тегированные кортежи как сумма, структуры как произведение, и исчерпывающий case:
Список — это «пусто или голова и хвост-список»: сумма единицы и произведения. Алгебраически $L \cong 1 + a\times L$:
Та же рекурсивная сумма-произведение лежит и под деревьями произвольной арности — а к ним мы вернёмся, когда речь пойдёт об оркестрации агентов как дереве надзора. Структура данных и структура системы — родня.
Типы складываются и умножаются, образуют полукольцо с нулём и единицей, подчиняются дистрибутивности, а функции дают степени. Считая обитателей, инженер делает недопустимые состояния невыразимыми; исчерпывающий разбор гарантирует, что учтён каждый вариант; рекурсивные типы описывают списки и деревья как уравнения. Алгебра из главы I буквально живёт в типах из главы VI.
Это естественный вход в следующую главу: когда состояния честно смоделированы, а разбор исчерпывающ, программа становится корректной по построению. О полной корректности — типах, тотальности и доказательствах — глава VII.