Теория категорий: объекты, морфизмы, функторы, естественные преобразования
Теория категорий заслужила две противоположные репутации. С одной стороны — «абстрактная чушь» (термин, кстати, придуман самими категорщиками — abstract nonsense, полушутливое самоназвание): куча стрелочек, ничего не вычисляется. С другой — «единственная математика, которая объясняет, почему код на самом деле собирается вместе».
Обе репутации заслуженны, и обе — про одно и то же свойство. Теория категорий сознательно отказывается смотреть внутрь объектов. Она не знает, что такое элемент множества, бит, строка или запись в базе. Она знает только: есть объекты, между ними есть стрелки, стрелки складываются друг с другом. И оказывается, что этого хватает, чтобы вывести огромное количество структуры — включая ту, которую вы каждый день руками пишете в коде.
Это делает её плохим инструментом для вычислений и превосходным — для проектирования. Когда вы решаете, «должен ли этот тип быть суммой или произведением», «почему Either и кортеж — двойственные вещи», «почему map обязан сохранять форму», «почему JOIN ведёт себя как декартово произведение с условием» — вы занимаетесь теорией категорий, просто без словаря.
Эта статья — про словарь и фундамент. Прикладная часть (монады, F-алгебры, линзы, свободные конструкции) — в следующей статье трека.
Три сцены, где вы уже трогали категории руками
Сцена 1. Ревью кода на map. Коллега пишет «оптимизацию»: вместо xs.map(f).map(g) — xs.map(x => g(f(x))). Все кивают: очевидно, эквивалентно. Но почему очевидно? Это не свойство списка. Это закон функтора: map(g) ∘ map(f) = map(g ∘ f). Он не выполняется автоматически — его нужно требовать. И существуют реализации map, которые его нарушают (см. ниже), после чего «очевидная» оптимизация ломает продакшн.
Сцена 2. Проектирование доменной модели. Нужно смоделировать «платёж — либо картой, либо через СБП». Вы выбираете между class Payment { card?: Card; sbp?: Sbp } и размеченным объединением Card | Sbp. Первый вариант допускает четыре состояния, из которых два невалидны. Второй — ровно два. Категорно: вам нужно копроизведение, а вы построили ослабленное произведение. Это ровно то различие, из которого выросла вся культура «make illegal states unrepresentable».
Сцена 3. Миграция схемы БД. Есть схема A, есть схема B, есть отображение таблиц и колонок. Вопрос «когда миграция корректна» — это вопрос «является ли отображение функтором»: сохраняются ли внешние ключи как композиции и не ломаются ли тождества. Дэвид Спивак довёл эту мысль до формальной теории функториальной миграции данных (arXiv:1009.1166), и на ней построен инструментарий CQL.
Ни одна сцена не требует знать, что такое предпучок. Требуется знать определение категории и функтора — и это буквально полстраницы текста.
Определение категории
Категория C состоит из:
1. Класса объектов Ob(C)
2. Для каждой пары объектов A, B —
множества морфизмов (стрелок) Hom(A, B), пишут также C(A, B) или A -> B
3. Операции композиции
∘ : Hom(B, C) × Hom(A, B) -> Hom(A, C)
4. Для каждого объекта A — тождественного морфизма
id_A ∈ Hom(A, A)
со следующими двумя законами (и это всё, больше в определении ничего нет):
(L1) Ассоциативность: h ∘ (g ∘ f) = (h ∘ g) ∘ f
для любых f: A -> B, g: B -> C, h: C -> D
(L2) Единица: f ∘ id_A = f = id_B ∘ f
для любого f: A -> B
Дополнительно требуется, чтобы Hom(A, B) и Hom(A', B') не пересекались при (A,B) ≠ (A',B'): у каждой стрелки есть ровно один источник (домен) и ровно одна цель (кодомен). Это техническая деталь, но она важна: стрелка f — это не «функция сама по себе», а функция вместе с объявленным типом. Ровно как в языке со статической типизацией: id :: Int -> Int и id :: String -> String — разные морфизмы.
Что здесь важно понять сразу
Первое: композиция — первична, элементы — вторичны. В теории множеств базовое понятие — «принадлежит». В теории категорий базовое понятие — «стрелка составляется со стрелкой». Всё остальное (элементы, подобъекты, произведения) приходится переопределять через стрелки. Это выглядит как самоограничение, но именно оно даёт переносимость: определение, сформулированное только через стрелки, автоматически имеет смысл в любой категории.
Второе: категория — это типизированный моноид. Сравните с определением моноида из статьи Абстрактная алгебра: множество, ассоциативная операция, нейтральный элемент. Категория — то же самое, но операция частичная: g ∘ f определена только если dst(f) = src(g). Объекты — это, по сути, метки типов, разрешающие или запрещающие композицию. Отсюда полезная мантра: «категория — это моноид, где не всё со всем перемножается».
Третье: размер имеет значение. Ob(C) — класс, а не множество, иначе не получится говорить про «категорию всех множеств» (парадокс Рассела, см. Теория множеств). Категория называется малой, если Ob(C) и все Hom(A,B) — множества; локально малой, если хотя бы все Hom(A,B) — множества. Set, Grp, Top локально малы, но не малы.
Обратите внимание на регулярность: на каждом уровне — данные плюс законы. Это единственный по-настоящему повторяющийся паттерн в теории категорий, и он же — рецепт того, как определять свои абстракции в коде.
Восемь категорий, из которых надо собрать интуицию
Одна-две модели в голове ведут к неверным обобщениям. Ниже — намеренно разнородный набор.
| Категория | Объекты | Морфизмы A -> B |
Композиция | id |
|---|---|---|---|---|
Set |
множества | функции | подстановка | x ↦ x |
Rel |
множества | бинарные отношения R ⊆ A×B |
реляционная композиция | диагональ |
Poset(P) |
элементы P |
ровно одна стрелка, если a ≤ b |
транзитивность | рефлексивность |
BM (моноид M) |
один объект * |
элементы M |
операция моноида | нейтральный |
Vect_k |
векторные пространства | линейные отображения | композиция отображений | тождественное |
Mat_k |
натуральные числа n |
матрицы m×n |
умножение матриц | единичная матрица |
Type |
типы языка | чистые функции | . / andThen |
identity |
Free(G) |
вершины графа G |
пути в графе | склейка путей | пустой путь |
Четыре наблюдения, которые ломают наивные ожидания:
- Морфизм — не обязательно функция. В
Relэто отношение, вMat_k— матрица, вFree(G)— путь. Композиция вRel— булево умножение матриц смежности; вот почему транзитивное замыкание графа и SQL-джойны выглядят как линейная алгебра над булевым полукольцом (подробнее — в Теории графов). - Между двумя объектами может быть не более одной стрелки (
Poset) — и категория всё равно полноценная. Такие категории называют тонкими: в них коммутативность любой диаграммы бесплатна. - Объектов может быть ровно один (
BM) — и тогда категория это просто моноид. Функтор изBMвSet— это в точности действие моноида на множестве. Vect_kиMat_k— разные категории, но эквивалентные. Каждая матрица задаёт линейное отображение, и каждое отображение между конечномерными пространствами после выбора базиса становится матрицей (см. Матрицы и линейные отображения). «Эквивалентность категорий» — более слабое и более правильное понятие, чем изоморфизм; к нему вернёмся.
Проверяем законы кодом
Конечную категорию можно задать таблицей композиции и проверить законы полным перебором. Сложность: O(|Mor|^3) по времени на ассоциативность и O(|Mor|^2) по памяти на таблицу — для учебных примеров это ничто, а ошибки ловит железно.
class FinCat:
"""Конечная категория, заданная явными таблицами."""
def __init__(self, objects, morphisms, ident, comp):
self.objects = list(objects)
self.morphisms = dict(morphisms) # имя -> (источник, цель)
self.ident = dict(ident) # объект -> имя тождественного морфизма
self.comp = dict(comp) # (g, f) -> имя морфизма g∘f
def src(self, f):
return self.morphisms[f][0]
def dst(self, f):
return self.morphisms[f][1]
def composable(self):
# пары (g, f), для которых определена композиция g∘f
return [(g, f) for g in self.morphisms for f in self.morphisms
if self.src(g) == self.dst(f)]
def check(self):
errs = []
# 1. композиция тотальна на составимых парах и имеет правильный тип
for g, f in self.composable():
if (g, f) not in self.comp:
errs.append(f"не определена композиция {g}∘{f}")
continue
h = self.comp[(g, f)]
if (self.src(h), self.dst(h)) != (self.src(f), self.dst(g)):
errs.append(f"{g}∘{f} = {h}: неверные источник/цель")
if errs: # дальше проверять бессмысленно: таблица «дырявая»
return errs
# 2. закон единицы (L2)
for A in self.objects:
i = self.ident[A]
if (self.src(i), self.dst(i)) != (A, A):
errs.append(f"id_{A} не является эндоморфизмом {A}")
for f in self.morphisms:
A, B = self.src(f), self.dst(f)
if self.comp.get((f, self.ident[A])) != f:
errs.append(f"правый закон единицы нарушен для {f}")
if self.comp.get((self.ident[B], f)) != f:
errs.append(f"левый закон единицы нарушен для {f}")
# 3. ассоциативность (L1)
for h in self.morphisms:
for g in self.morphisms:
if self.dst(g) != self.src(h):
continue
for f in self.morphisms:
if self.dst(f) != self.src(g):
continue
if self.comp[(self.comp[(h, g)], f)] != self.comp[(h, self.comp[(g, f)])]:
errs.append(f"ассоциативность нарушена: {h}∘{g}∘{f}")
return errs
def poset_category(n):
"""Категория из порядка (<=) на {0, ..., n-1}: стрелка i -> j есть, если i <= j."""
objs = list(range(n))
mors = {f"f{i}{j}": (i, j) for i in objs for j in objs if i <= j}
ident = {i: f"f{i}{i}" for i in objs}
comp = {(f"f{j}{k}", f"f{i}{j}"): f"f{i}{k}"
for i in objs for j in objs for k in objs if i <= j <= k}
return FinCat(objs, mors, ident, comp)
def monoid_category(n):
"""Моноид Z/n как категория с одним объектом."""
mors = {f"m{a}": ("*", "*") for a in range(n)}
comp = {(f"m{a}", f"m{b}"): f"m{(a + b) % n}" for a in range(n) for b in range(n)}
return FinCat(["*"], mors, {"*": "m0"}, comp)
P, M = poset_category(3), monoid_category(3)
print("порядок <= на {0,1,2}:", P.check() or "категория ✓")
print("моноид Z/3 :", M.check() or "категория ✓")
# намеренно портим одну ячейку таблицы композиции
broken = FinCat(P.objects, P.morphisms, P.ident, {**P.comp, ("f12", "f01"): "f00"})
print("сломанная таблица :", broken.check())
порядок <= на {0,1,2}: категория ✓
моноид Z/3 : категория ✓
сломанная таблица : ['f12∘f01 = f00: неверные источник/цель']
Коммутативные диаграммы: как категорщики пишут уравнения
Диаграмма — это ориентированный граф, вершины которого помечены объектами, а рёбра морфизмами. Диаграмма коммутирует, если любые два пути с общим началом и общим концом дают равные композиции.
Это не декорация, а нотация: коммутативная диаграмма — компактная запись системы уравнений. Треугольник
A ---f---> B
\ /
h g
\ /
v v
C
означает ровно одно уравнение g ∘ f = h. Квадрат означает одно уравнение. Куб из шести квадратов — шесть уравнений, из которых часть обычно следует из остальных. Умение «читать диаграммы» — это умение мгновенно превращать картинку в уравнения и обратно.
Практический совет: когда вы застряли на категорном определении, нарисуйте его. Почти все определения в этой статье — это одна диаграмма плюс слово «единственный».
Изоморфизм, мономорфизм, эпиморфизм
Изоморфизм
f: A -> B — изоморфизм, если существует g: B -> A с
g ∘ f = id_A и f ∘ g = id_B
Такой g единственен (стандартное упражнение: если g и g' оба обратные, то g = g ∘ id = g ∘ (f ∘ g') = (g ∘ f) ∘ g' = id ∘ g' = g'), его обозначают f⁻¹. Объекты A ≅ B называют изоморфными.
Что такое изоморфизм в разных категориях:
- в
Set— биекция; - в
Grp,Ring,Vect— изоморфизм соответствующих структур; - в
Poset— равенство (антисимметрия:a ≤ bиb ≤ aдаютa = b); - в
Top— гомеоморфизм, а не непрерывная биекция (обратное отображение тоже обязано быть непрерывным); - в
Type— пара функцийto/from, взаимно обратных. Например,(A, ()) ≅ AиEither<A, Void> ≅ A.
Ключевая идея: в теории категорий равенство объектов не используется, используется изоморфизм. Формулировка «единственный с точностью до единственного изоморфизма» — это категорный аналог слова «канонический», и именно она делает универсальные свойства работающими.
Мономорфизм и эпиморфизм: осторожно
Как определить «инъективность», не имея элементов? Через сократимость.
f: A -> B — мономорфизм, если для любых g, h: X -> A
из f ∘ g = f ∘ h следует g = h (сокращение слева)
f: A -> B — эпиморфизм, если для любых g, h: B -> Y
из g ∘ f = h ∘ f следует g = h (сокращение справа)
В Set моно = инъекция, эпи = сюръекция. И вот здесь — самое частое заблуждение новичка: считать, что так везде.
Контрпример, который стоит запомнить. В категории моноидов Mon вложение i: (N, +) -> (Z, +) не сюръективно, но является эпиморфизмом: если два гомоморфизма моноидов g, h: Z -> Y совпадают на всех натуральных числах, они совпадают и на отрицательных, потому что g(-n) вынужденно равен обратному к g(n). Аналогично в категории колец Z -> Q — эпиморфизм, не будучи сюръекцией.
Практический вывод: «моно + эпи» не влечёт «изо». Изоморфизм — более сильное требование, и в Set совпадение этих понятий — приятная случайность, а не общий закон.
Двойственность: одна теорема — две теоремы
Для любой категории C определена противоположная категория C^op: те же объекты, а Hom_{C^op}(A, B) = Hom_C(B, A), композиция «наоборот»: f ∘_op g = g ∘_C f. Проверка законов тривиальна.
Это выглядит как формальный трюк, но у него огромные последствия. Принцип двойственности: если утверждение доказано для всех категорий, то верно и утверждение, полученное разворотом всех стрелок. Вы доказываете одну теорему — получаете две.
Двойственные пары, которые надо знать наизусть:
мономорфизм <--> эпиморфизм
начальный объект <--> терминальный объект
произведение <--> копроизведение
предел <--> копредел
pullback <--> pushout
алгебра функтора <--> коалгебра функтора
В программировании эта симметрия видна как «данные против кодданных»: списки/деревья (индуктивные, алгебры, строятся снизу) против потоков/процессов (коиндуктивные, коалгебры, наблюдаются сверху). Эту линию мы развернём в следующей статье.
Начальные и терминальные объекты
Объект 0 — начальный, если для каждого A существует ровно один морфизм 0 -> A
Объект 1 — терминальный, если для каждого A существует ровно один морфизм A -> 1
Теорема. Начальный объект, если существует, единственен с точностью до единственного изоморфизма.
Доказательство в две строки: пусть 0 и 0' — начальные. Есть единственные u: 0 -> 0' и v: 0' -> 0. Тогда v ∘ u: 0 -> 0 — морфизм из начального объекта в себя, но такой ровно один, и id_0 уже подходит; значит v ∘ u = id_0. Симметрично u ∘ v = id_{0'}. Это шаблон доказательства, который повторяется для всех универсальных конструкций.
Примеры:
| Категория | Начальный | Терминальный |
|---|---|---|
Set |
∅ |
любой одноэлементный {*} |
Type |
Void / Never (необитаемый тип) |
() / unit |
Poset |
наименьший элемент | наибольший элемент |
Grp |
тривиальная группа | тривиальная группа (совпадают!) |
Rng (кольца с 1) |
Z |
нулевое кольцо |
Программистское прочтение: функция Never -> A существует ровно одна и никогда не вызывается (в TypeScript это absurd), функция A -> unit существует ровно одна и выбрасывает значение. Терминальный объект — это ещё и способ говорить об «элементах» без элементов: точка объекта A — это морфизм 1 -> A. В Set точки {*} -> A в точности соответствуют элементам A.
Универсальные свойства: произведение и копроизведение
Здесь теория категорий начинает окупаться. Вместо того чтобы строить объект, мы описываем его роль — и получаем определение, переносимое куда угодно.
Определение. Произведение объектов A и B — это объект P вместе с морфизмами p1: P -> A, p2: P -> B, такими что для любого объекта X и любой пары морфизмов f: X -> A, g: X -> B существует единственный m: X -> P с
p1 ∘ m = f и p2 ∘ m = g
Разберём по словам. «Любой X с парой стрелок» — это все возможные способы «одновременно смотреть на A и на B». «Существует единственный m» — значит P лучший такой способ: любой другой пропускается через него ровно одним образом. Произведение — не «множество пар», а «оптимальный наблюдатель за парой объектов».
Что получается в конкретных категориях:
Set— декартово произведениеA × B,m(x) = (f(x), g(x));Type— кортеж(A, B), аm— этоx => [f(x), g(x)];Poset— точная нижняя граньinf(a, b)(в решётке — операцияmeet);Vect— прямая суммаV ⊕ W;Grp— прямое произведение групп;- в логике (объекты = высказывания, стрелка = следование) — конъюнкция
A ∧ B.
Один и тот же чертёж, шесть разных «реализаций». Отсюда же бесплатно следуют факты вроде A × B ≅ B × A и (A × B) × C ≅ A × (B × C): обе стороны удовлетворяют одному универсальному свойству, значит изоморфны. Обратите внимание — изоморфны, а не равны: ((a,b),c) и (a,(b,c)) в памяти лежат по-разному, и именно поэтому в языках с кортежами приходится писать явные конвертеры.
from itertools import product as cart
# --- произведение в Set ---
def pi1(p): return p[0]
def pi2(p): return p[1]
def mediator(f, g): return lambda x: (f(x), g(x))
A, B, X = ["a", "b"], [0, 1], ["x", "y", "z"]
f = {"x": "a", "y": "b", "z": "a"}.__getitem__
g = {"x": 1, "y": 1, "z": 0}.__getitem__
m = mediator(f, g)
print("p1∘m == f :", all(pi1(m(x)) == f(x) for x in X)) # True
print("p2∘m == g :", all(pi2(m(x)) == g(x) for x in X)) # True
# честная проверка единственности: перебираем ВСЕ функции X -> A×B
all_maps = [dict(zip(X, c)).__getitem__ for c in cart(list(cart(A, B)), repeat=len(X))]
good = [h for h in all_maps if all(pi1(h(x)) == f(x) and pi2(h(x)) == g(x) for x in X)]
print("медиаторов ровно:", len(good)) # 1
# --- копроизведение: A + B ---
def inl(a): return ("L", a)
def inr(b): return ("R", b)
def comediator(f, g): return lambda t: f(t[1]) if t[0] == "L" else g(t[1])
h = comediator(lambda a: a.upper(), lambda b: str(b * 10))
print("копроизведение:", [h(inl("a")), h(inr(3))]) # ['A', '30']
Копроизведение — это то же самое в C^op: объект A + B с инъекциями i1: A -> A+B, i2: B -> A+B, такими что любая пара f: A -> Y, g: B -> Y пропускается через единственный [f, g]: A+B -> Y. В Set это дизъюнктное объединение, в типах — размеченное объединение (Either, enum в Rust, discriminated union в TypeScript), в Poset — sup, в логике — дизъюнкция.
Именно поэтому сцена 2 из вступления решается однозначно: «либо карта, либо СБП» — это Card + Sbp, и медиатор comediator — это ровно switch по тегу, который компилятор может проверить на полноту. Смотрите также трек Типы и TypeScript — там это живёт под именем discriminated unions.
Пределы: pullback как INNER JOIN
Произведение и терминальный объект — частные случаи предела (limit): универсального конуса над диаграммой. Самый полезный для инженера случай — расслоённое произведение (pullback): предел диаграммы A -> K <- B.
A ×_K B = { (a, b) ∈ A × B | f(a) = g(b) }
Это буквально INNER JOIN по ключу. И это не метафора — это одно и то же определение.
результат JOIN"] O["orders"] U["users"] K["K = множество user_id"] X["любая таблица X
с согласованной парой стрелок"] P -- "p1" --> O P -- "p2" --> U O -- "f = orders.user_id" --> K U -- "g = users.id" --> K X -. "единственный медиатор" .-> P X -- "u" --> O X -- "v" --> U
Условие коммутативности f ∘ p1 = g ∘ p2 — это в точности ON orders.user_id = users.id. Универсальность означает: результат JOIN содержит все согласованные пары и ничего лишнего.
def pullback(dom_f, f, dom_g, g):
"""Расслоённое произведение: {(x, y) | f(x) = g(y)} плюс две проекции."""
pairs = [(x, y) for x in dom_f for y in dom_g if f[x] == g[y]]
return pairs, (lambda p: p[0]), (lambda p: p[1])
users = {1: ("ann", 10), 2: ("bob", 20), 3: ("cid", 10)}
orders = {"o1": (1, 5), "o2": (1, 7), "o3": (3, 2)}
f = {o: orders[o][0] for o in orders} # orders -> user_id
g = {u: u for u in users} # users -> user_id
pairs, p1, p2 = pullback(list(orders), f, list(users), g)
print(sorted((p1(p), p2(p)) for p in pairs))
# [('o1', 1), ('o2', 1), ('o3', 3)]
Двойственная конструкция — pushout — это «склейка по общей части»: в системах контроля версий это трёхсторонний merge (общий предок K, две ветки A и B, результат — pushout), в топологии — склейка пространств.
Функторы: отображения между категориями
Категория — структура. Значит, есть осмысленное понятие «сохраняющего структуру отображения».
Определение. Функтор F: C -> D — это:
1. Отображение объектов: A ∈ Ob(C) ↦ F(A) ∈ Ob(D)
2. Отображение стрелок: f: A -> B ↦ F(f): F(A) -> F(B)
с двумя законами:
(F1) F(id_A) = id_{F(A)} сохранение тождеств
(F2) F(g ∘ f) = F(g) ∘ F(f) сохранение композиции
Такой функтор называют ковариантным. Контравариантный функтор разворачивает стрелки: F(f): F(B) -> F(A) и F(g ∘ f) = F(f) ∘ F(g). Формально контравариантный функтор C -> D — это просто ковариантный функтор C^op -> D.
Зоопарк функторов
List,Maybe,Set,Tree— эндофункторы наType:List(A)— тип,List(f) = map f. Это те, которые все знают.- Функтор степенного множества
P: Set -> Set:P(A)— множество подмножеств,P(f)(S) = {f(s) | s ∈ S}— прямой образ. Ковариантный. - Обратный образ
P*: Set^op -> Set:P*(f)(T) = f⁻¹(T). Контравариантный. Тот же «носитель», другая вариантность. - Забывающий функтор
U: Mon -> Set: моноиду сопоставляет его несущее множество, гомоморфизму — ту же функцию. Он ничего не «содержит» — просто теряет структуру. Отличный аргумент против интуиции «функтор = контейнер». - Свободный функтор
F: Set -> Mon: множествуAсопоставляет свободный моноидA*(списки). ПараF ⊣ U— сопряжённые функторы, важнейшая конструкция; она в следующей статье. - Hom-функторы.
Hom(A, -): C -> Setковариантен:Hom(A, f)(u) = f ∘ u. В коде этоmapдля функционального типа:(A -> X) ↦ (A -> Y). АHom(-, B): C^op -> Setконтравариантен:Hom(f, B)(u) = u ∘ f, в коде — «предкомпозиция», ровно то, почему аргументы функций контравариантны при проверке подтипов в TypeScript. - Функтор между тонкими категориями — это в точности монотонная функция между порядками.
- Функтор из
BMвSet— действие моноида на множестве; изBMвVect_k— представление моноида.
Законы функтора нарушаются легко
# правильный функтор
def fmap(f, xs): return [f(x) for x in xs]
# «функтор», который заодно разворачивает список
def bad_fmap(f, xs): return [f(x) for x in reversed(xs)]
print(bad_fmap(lambda x: x, [1, 2, 3])) # [3, 2, 1] != [1, 2, 3] -> нарушен F1
print(bad_fmap(lambda x: x + 1, bad_fmap(lambda x: x * 2, [1, 2, 3]))) # [3, 5, 7]
print(bad_fmap(lambda x: x * 2 + 1, [1, 2, 3])) # [7, 5, 3] -> нарушен F2
Отсюда мораль для ревью: если вы пишете свой map/fmap/Select/select, законы функтора — это не философия, а обязательные property-тесты. Оптимизации компилятора (fusion в GHC, map/map в Scala и Kotlin) переписывают код, предполагая F2. Нарушите — получите разное поведение с оптимизацией и без.
Проверяем функтор кодом
def check_functor(C, D, on_obj, on_mor):
"""on_obj: объект C -> объект D; on_mor: имя морфизма C -> имя морфизма D."""
errs = []
for f, (A, B) in C.morphisms.items(): # типизация
Ff = on_mor[f]
if (D.src(Ff), D.dst(Ff)) != (on_obj[A], on_obj[B]):
errs.append(f"F({f}) имеет неверный тип")
for A in C.objects: # (F1)
if on_mor[C.ident[A]] != D.ident[on_obj[A]]:
errs.append(f"F(id_{A}) != id_F({A})")
for (g, f), gf in C.comp.items(): # (F2)
if D.comp[(on_mor[g], on_mor[f])] != on_mor[gf]:
errs.append(f"F({g}∘{f}) != F({g})∘F({f})")
return errs
# Функтор из порядка (0 <= 1 <= 2) в моноид Z/3: стрелка i -> j идёт в разность j - i
on_obj = {i: "*" for i in P.objects}
on_mor = {f"f{i}{j}": f"m{(j - i) % 3}" for i in range(3) for j in range(3) if i <= j}
print(check_functor(P, M, on_obj, on_mor) or "функтор ✓") # функтор ✓
bad = {**on_mor, "f01": "m2"}
print(check_functor(P, M, on_obj, bad))
# ['F(f12∘f01) != F(f12)∘F(f01)']
Функтор здесь «измеряет длину пути» в порядке — типичный пример того, как функтор переносит задачу из одной категории в другую, где она проще. Ровно так работают все инварианты в топологии: фундаментальная группа π1: Top* -> Grp — функтор, и невозможность непрерывного отображения доказывается через невозможность гомоморфизма групп.
Естественные преобразования: «морфизмы между функторами»
Эйленберг и Мак-Лейн придумали категории и функторы ради этого понятия — в статье 1945 года они прямо пишут, что функторы понадобились, чтобы определить естественные преобразования (General Theory of Natural Equivalences, Trans. AMS 58). До этого «естественность» изоморфизма была неформальным словом, которое все понимали, но никто не мог определить.
Определение. Пусть F, G: C -> D — функторы. Естественное преобразование α: F ⇒ G — это семейство морфизмов α_A: F(A) -> G(A), по одному на каждый объект A ∈ Ob(C), такое что для любого морфизма f: A -> B коммутирует квадрат:
G(f) ∘ α_A = α_B ∘ F(f)
Читать это надо так: α перестраивает форму контейнера, F(f)/G(f) меняют содержимое. Условие естественности говорит, что эти две операции коммутируют — то есть α не имеет права смотреть на содержимое. Она видит только структуру.
Примеры и контрпримеры
safeHead: List ⇒ Maybe — естественное преобразование:
Maybe(f)(safeHead(xs)) = safeHead(List(f)(xs))
Слева: взяли голову, потом применили f. Справа: применили f ко всем, потом взяли голову. Одно и то же — потому что safeHead смотрит только на длину.
А вот firstEven («первый чётный элемент») — не естественное преобразование, хотя типы те же:
import random
def fmap_list(f, xs): return [f(x) for x in xs]
def fmap_maybe(f, m): return None if m is None else f(m)
def safe_head(xs): return xs[0] if xs else None
def first_even(xs): return next((x for x in xs if x % 2 == 0), None)
def naturality_holds(alpha, f, samples):
# G(f) ∘ α == α ∘ F(f), здесь F = List, G = Maybe
return all(fmap_maybe(f, alpha(xs)) == alpha(fmap_list(f, xs)) for xs in samples)
random.seed(7)
samples = [[random.randrange(10) for _ in range(random.randrange(5))] for _ in range(300)]
funcs = [lambda x: x + 1, lambda x: x * x, lambda x: -x]
print("safe_head :", all(naturality_holds(safe_head, f, samples) for f in funcs)) # True
print("first_even:", all(naturality_holds(first_even, f, samples) for f in funcs)) # False
xs = [1, 2, 3]
print(fmap_maybe(lambda x: x + 1, first_even(xs)), # 3 (взяли 2, прибавили 1)
first_even(fmap_list(lambda x: x + 1, xs))) # 2 (стало [2,3,4], первый чётный 2)
Разница принципиальная: first_even заглядывает в значения (проверяет чётность), поэтому её результат зависит от того, что за элементы лежат внутри. safe_head работает с формой.
Естественность = параметричность
И вот важнейший мост к программированию. В языке с параметрическим полиморфизмом функция типа
forall a. F a -> G a
автоматически естественна — иначе она смогла бы различить значения типа a, чего система типов не позволяет. Это следствие теоремы о параметричности Рейнольдса; популярное изложение — Филип Уодлер, «Theorems for Free!», 1989.
Практический эффект: сигнатура forall a. [a] -> Maybe a уже гарантирует, что функция может только выбрать элемент по позиции (или вернуть Nothing) — она физически не способна фильтровать по значению. Тип сам доказывает теорему. Именно поэтому «сделать функцию максимально полиморфной» — это не эстетика, а способ сузить пространство возможных реализаций до правильных.
Категория функторов
Естественные преобразования можно композировать покомпонентно: (β ∘ α)_A = β_A ∘ α_A. Проверка законов сводится к склейке квадратов. В итоге для любых C, D получается категория функторов [C, D] (пишут также D^C):
- объекты — функторы
C -> D; - морфизмы — естественные преобразования;
id_F— семействоid_{F(A)}.
Естественный изоморфизм — изоморфизм в [C, D], то есть семейство α_A, каждый компонент которого обратим. Формулировка «X и Y естественно изоморфны» — самая сильная форма утверждения «это одно и то же»: изоморфизм есть и он не требует произвольного выбора. Классика: конечномерное пространство V изоморфно V* (двойственному), но не естественно — нужен выбор базиса; а V ≅ V** естественно. См. Линейная алгебра: векторы.
Есть ещё горизонтальная композиция преобразований, из-за чего Cat (категория малых категорий) на самом деле 2-категория, но это уже за пределами базового курса.
Экспоненциалы и Карри–Ховард–Ламбек
Категория декартово замкнута (CCC), если в ней есть терминальный объект, все бинарные произведения и экспоненциалы: объект B^A с морфизмом eval: B^A × A -> B, такой что для любого f: X × A -> B есть единственный curry(f): X -> B^A с eval ∘ (curry(f) × id_A) = f.
Расшифровка: B^A — это «тип функций из A в B», eval — применение, а curry — то самое каррирование, которое вы пишете каждый день. Универсальное свойство утверждает: функция двух аргументов и функция, возвращающая функцию, — одно и то же.
Hom(X × A, B) ≅ Hom(X, B^A)
Отсюда — соответствие Карри–Ховарда–Ламбека, тройной словарь:
| Логика | Типы | Категория |
|---|---|---|
| высказывание | тип | объект |
| доказательство | программа | морфизм |
A ∧ B |
(A, B) |
произведение |
A ∨ B |
Either A B |
копроизведение |
A ⇒ B |
A -> B |
экспоненциал |
true |
unit |
терминальный объект |
false |
Void |
начальный объект |
| упрощение доказательства | вычисление | коммутирующая диаграмма |
Строго: типизированное лямбда-исчисление с произведениями и декартово замкнутые категории — эквивалентные понятия (Ламбек, 1980; каноническое изложение — Lambek & Scott, Introduction to Higher Order Categorical Logic). Это не аналогия: это теорема об эквивалентности. Логическая часть словаря разобрана в статье Математическая логика и доказательства, вычислительная — в Теории вычислимости.
Важная оговорка: Type реального языка — не настоящая CCC. Мешают незавершающиеся вычисления, исключения, null, побочные эффекты. Hask — полезная фикция, а не факт; см. подробный разбор на nLab. Пользоваться этим соответствием стоит как проектным ориентиром, а не как гарантией.
Лемма Йонеды за пять минут
Формулировка выглядит устрашающе:
Nat( Hom(A, -), F ) ≅ F(A) естественно по A и по F
Интуиция: слева — все естественные способы «наблюдать» объект A через функтор F; справа — просто значение F(A). Утверждение: наблюдений ровно столько, сколько значений. Объект полностью определяется тем, как остальные объекты на него смотрят.
Аналогия из инженерии: если два сервиса неотличимы по всему множеству возможных запросов и ответов, они одинаковы. Тестирование через публичный интерфейс — это Йонеда в быту.
В коде это CPS-преобразование:
# Йонеда для списков: F(A) ≅ для любого R: (A -> R) -> F(R)
def to_yoneda(xs): return lambda k: [k(x) for x in xs]
def from_yoneda(cps): return cps(lambda a: a) # подставляем id — ключевой шаг доказательства
xs = [1, 2, 3]
print(from_yoneda(to_yoneda(xs)) == xs) # True
print(to_yoneda(xs)(lambda n: n * n)) # [1, 4, 9]
Доказательство леммы Йонеды — это ровно строка cps(lambda a: a): естественное преобразование целиком определяется своим значением на id_A. Отсюда же берутся Church-кодирование, difference lists, оптика и «Йонеда-трюк» для устранения промежуточных структур в библиотеках вроде lens и optics-ts.
Карта понятий
Типичные заблуждения
«Теория категорий — это про монады в Haskell». Монада — одно определение из сотен, и появилось оно в информатике только в 1991 году. Базовый багаж — категория, функтор, естественное преобразование, универсальное свойство, двойственность. Монады без этого выучиваются как заклинание.
«Категория — это множество объектов со структурой». Объекты почти неважны; вся информация в Hom-множествах. Категорию с одним объектом (моноид) невозможно понять, глядя на объекты. И Ob(C) — класс, а не множество.
«Функтор — это контейнер». Забывающий функтор Mon -> Set ничего не содержит. Hom(-, B) контравариантен и «контейнером» не является ни в каком смысле. Функтор — это согласованный перевод стрелок, не более.
«Мономорфизм = инъекция, эпиморфизм = сюръекция». Верно в Set, ложно в Mon, Rng, Top. Считайте это свойством Set, а не определением.
«Изоморфные объекты равны». Изоморфны — значит взаимозаменяемы по всем категорным свойствам. Но ((a,b),c) и (a,(b,c)) изоморфны и различны в памяти; сериализация, ABI и производительность живут именно в этой разнице.
«Универсальное свойство — просто вычурная формулировка конструкции». Наоборот: конструкция — одна из реализаций, универсальное свойство — спецификация. Это в точности «интерфейс против реализации», и польза та же.
«Диаграммы коммутируют сами собой». Коммутативность — это утверждение, которое нужно доказывать. Единственное исключение — тонкие категории, где стрелка между парой объектов не более одной.
«Это даст мне производительность». Не даст. Даст переиспользуемые законы, корректные абстракции и точный язык для проектных решений. Оптимизации типа map-fusion — приятный побочный эффект законов, а не цель.
Где это реально используется
Системы типов и языки. Иерархия Functor / Applicative / Monad / Traversable в Haskell (документация base) и в Scala Cats (typelevel.org/cats) — это прямая транскрипция категорных определений вместе с законами, которые проверяются property-тестами. В Rust Iterator::map, в C# LINQ Select, в Elixir Enum.map — та же алгебра, только без формулировки законов; см. трек Elixir.
Оптимизирующие компиляторы. Правила переписывания вроде map f . map g -> map (f . g) в GHC (RULES-прагмы) обоснованы законом F2. Аналогично устроены fusion-оптимизации в Spark Catalyst и в LLVM для цепочек трансформаций.
Базы данных и интеграция. Функториальная миграция данных Спивака (arXiv:1009.1166) описывает схему как категорию, инстанс — как функтор в Set, а миграцию — как функтор между схемами; три вида миграции (Δ, Σ, Π) — это сопряжённые функторы. Инженерное следствие практично: если ваше отображение схем — функтор, миграция гарантированно сохраняет ссылочную целостность.
Распределённые системы. CRDT — это полурешётки объединения, то есть частичные порядки с копределами; сходимость реплик доказывается тем, что merge — это sup, ассоциативный, коммутативный и идемпотентный. Логика monoid-гомоморфизмов лежит в основе агрегатов в потоковых системах.
Оптика и работа с данными. Линзы, призмы и траверсалы (lens в Haskell, optics-ts, monocle-ts) выводятся из Йонеды и представления через функторы. Практика — иммутабельные обновления вложенных структур во фронтенде и в event sourcing.
Верификация и proof assistants. Coq, Agda, Lean построены на теории типов, для которой CCC и локально декартово замкнутые категории — семантика. Гомотопическая теория типов — прямое продолжение этой линии.
Мини-итог
- Категория — объекты, стрелки, ассоциативная композиция и единицы. Это типизированный моноид: не всё со всем составляется.
- Морфизм не обязан быть функцией; объекты не обязаны быть множествами. Вся информация — в
Hom-множествах. - Изоморфизм заменяет равенство. «Единственный с точностью до единственного изоморфизма» — категорное «канонический».
- Двойственность даёт вторую теорему бесплатно: моно/эпи, произведение/копроизведение, предел/копредел, алгебра/коалгебра.
- Универсальные свойства описывают роль объекта, а не его устройство. Произведение — это кортеж и
ANDиinfодновременно; копроизведение — sum-тип иORиsup. - Функтор переносит структуру между категориями; его два закона — обязательные property-тесты для любого вашего
map. - Естественное преобразование — «одинаковое поведение на всех объектах сразу». В языке с параметрическим полиморфизмом естественность выдаётся бесплатно вместе с типом.
- Лемма Йонеды: объект определяется тем, как на него смотрят.
Источники
- Saunders Mac Lane. Categories for the Working Mathematician, 2nd ed. Springer GTM 5 — springer.com. Канонический справочник; читать после введения.
- Steve Awodey. Category Theory. Oxford Logic Guides — global.oup.com. Лучший строгий вход для тех, кто не математик по образованию.
- Emily Riehl. Category Theory in Context — свободный PDF: math.jhu.edu/~eriehl/context.pdf.
- Bartosz Milewski. Category Theory for Programmers — github.com/hmemcpy/milewski-ctfp-pdf, видеокурс и блог: bartoszmilewski.com.
- Brendan Fong, David Spivak. Seven Sketches in Compositionality: An Invitation to Applied Category Theory — arXiv:1803.05316.
- Samuel Eilenberg, Saunders Mac Lane. General Theory of Natural Equivalences, Trans. AMS 58 (1945) — ams.org. Статья, с которой всё началось.
- Philip Wadler. Theorems for Free! (1989) и материалы по параметричности — homepages.inf.ed.ac.uk/wadler.
- Eugenio Moggi. Notions of Computation and Monads, Information and Computation 93 (1991) — PDF.
- David Spivak. Functorial Data Migration — arXiv:1009.1166.
- nLab — живая энциклопедия: ncatlab.org/nlab/show/category.
Что дальше
Мы построили словарь: категория, функтор, естественное преобразование, универсальное свойство, двойственность, Йонеда. Теперь у всего этого появятся имена из повседневного кода.
Дальше — Теория категорий в программировании: функторы, монады, F-алгебры, линзы: сопряжённые функторы и свободные конструкции, монады как моноиды в категории эндофункторов, аппликативы и траверсы, F-алгебры и катаморфизмы для разбора и свёртки деревьев, коалгебры для потоков, оптика как композиция доступа к данным — и разбор того, где эти абстракции реально окупаются, а где становятся оверинжинирингом.