Category Theory в CS

Почему TypeScript имеет intersection types? Почему async/await ведёт себя как монада? Почему линзы компонуются как функции? За всем этим стоит теория категорий. Это не случайность: лучшие конструкции в языках программирования - это категорные конструкции. Понять их математически - значит предсказывать, какие конструкции будут работать, ещё до написания кода.

• **Control.Lens в Haskell**: библиотека линз реализует профункторные оптики. Composable, typesafe, efficient - все свойства следуют из категорной теории. `(.)` - категорная композиция естественных преобразований
• **Idris, Agda, Coq**: языки с зависимыми типами - это реализации Мартин-Лёфовской теории типов, которая соответствует локально декартово замкнутым категориям. Доказательства = программы по Карри-Говарду
• **Scala Cats / Haskell mtl**: библиотеки эффектов реализуют Freyd-categories (монады с дополнительной структурой). Tagless Final - вложение в категорию T-алгебр

Предварительные знания

• Monads in Category Theory

Types As Objects

Типы в языке программирования ведут себя как объекты категории: у них есть морфизмы (функции), произведения (пары), копроизведения (sum types), экспоненциалы (функциональные типы). Это не метафора - категория **Hask** (Haskell-типы) является **декартово замкнутой категорией** (cartesian closed category, CCC), и именно это объясняет, почему функциональное программирование работает.

**Декартово замкнутая категория** (CCC) - категория с: 1. терминальным объектом 1 2. конечными произведениями A × B 3. экспоненциалами B^A = (A → B), удовлетворяющими curry: Hom(X × A, B) ≅ Hom(X, B^A). Категория Hask - CCC. Каждый функциональный язык реализует CCC.

**Изоморфизм Карри-Говарда**: типы ↔ логические формулы, программы ↔ доказательства. Product type соответствует конъюнкции (∧), Sum type - дизъюнкции (∨), функция - импликации (→), Never - ложи (⊥), Unit - истине (⊤). Написать функцию типа `(A, B) => A` - то же, что доказать P ∧ Q → P. Этот изоморфизм объясняет, почему системы типов и логика так похожи.

Denotational

**Денотационная семантика** - это способ придать программе математическое значение (денотат), не зависящее от деталей выполнения. Функция `f :: Int -> Int` - это математическая функция ℤ → ℤ. Нерекурсивные программы просто; рекурсия требует решения уравнений. Категорная теория (домены Скотта) предоставляет инструменты.

**Денотационная семантика** языка L - это функтор [[·]]: L → D из категории программ в математическую категорию D. Для Haskell D - категория CPO (complete partial orders) или DCPO: частично упорядоченных множеств с наименьшими верхними гранями направленных подмножеств. Рекурсия = наименьшая неподвижная точка по теореме Тарского.

**Категории доменов Скотта**: объекты - CPO (упорядоченные множества с наименьшим элементом ⊥ и направленными супремумами), морфизмы - непрерывные (Scott-continuous) функции, сохраняющие directed joins. Теорема Кнастера-Тарского: монотонная функция на полной решётке имеет наименьшую неподвижную точку. Это математическое основание рекурсии.

Современные альтернативы: **Axiomatic Semantics** (Флойд-Хоар), **Operational Semantics** (структурная операционная семантика Плоткина). Денотационная семантика - наиболее математически «чистая», но сложнее для конкурентности и эффектов. Категории используются во всех трёх: категории переходов, логики Хоара и т.д.

Profunctors

**Профунктор** (distributor, bimodule) - это «обобщённое соответствие» между двумя категориями. Функтор F: C → D можно рассматривать как профунктор через Hom_D(-, F(-)): C^{op} × D → Set. Профункторы обобщают как функторы, так и просто отношения. Они образуют **бикатегорию Prof**, мощную альтернативу Cat для многих задач.

**Профунктор** P: C ↛ D - это функтор P: D^{op} × C → Set. Тождественный профунктор id_C = Hom_C: C^{op} × C → Set. Композиция профункторов P: B ↛ C и Q: C ↛ D: (Q ∘ P)(b, d) = ∫^c P(b, c) × Q(c, d) (копредел над объектами C - «интеграл по концу»).

**Зачем профункторы**: они обобщают функторы и дают удобный язык для описания «соответствий» между данными. **Конец** (end) профунктора ∫_c P(c,c) - «глобальные элементы», естественные по c. Лемма Ёнеды через конец: Nat(F, G) ≅ ∫_c F(c) → G(c). Профункторы также основа теории **оптик** - компонуемых линз и призм.

Optics

**Оптики** (optics) - обобщение «линз» из функционального программирования. Линза позволяет «смотреть» (get) и «модифицировать» (set/over) часть структуры данных в чисто функциональном стиле. Теория категорий даёт математическое основание: **профункторная оптика** - это точное категорное определение, унифицирующее линзы, призмы, траверсы и другие оптики.

**Профункторная оптика** (optic) типа O(S, T, A, B) - это естественное преобразование: для любого профунктора P: Set ↛ Set, функция O(S, T, A, B) = ∀P. P(A, B) → P(S, T). Линза (Lens) - это оптика, где P ограничен на «Strong» профункторы; призма (Prism) - на «Choice» профункторы. Это элегантная унификация через Yoneda.

**Экзистенциальная кодировка**: альтернативная формулировка оптик через экзистенциальные типы. Lens S T A B = ∃R. (S → R × A) × (R × B → T). Это «хранение остатка» R при разборке S на (R, A) и сборке обратно из (R, B). Профункторная и экзистенциальная кодировки изоморфны - что следует из леммы Ёнеды!

Ключевые идеи

• **Types as objects**: язык программирования с произведениями, суммами и функциями = декартово замкнутая категория (CCC). Curry/uncurry - изоморфизм из аксиомы экспоненциала
• **Денотационная семантика**: программа = морфизм в CPO; рекурсия = наименьшая неподвижная точка по Тарскому; семантический функтор [[·]] сохраняет категорную структуру
• **Профункторы** P: D^{op} × C → Set обобщают функторы и отношения; конец ∫ - мощный инструмент для формулировки леммы Ёнеды и естественных преобразований
• **Оптики** (линзы, призмы, траверсы) = профункторные естественные преобразования; компонуются как морфизмы; единая категорная конструкция за всеми видами оптик

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

Теория категорий в CS опирается на все предыдущие концепции:

• Монады в программировании — Практическая основа: Maybe, List, IO - категорные монады на CCC типов
• Category Theory на собеседовании — Следующий урок: как объяснить все эти концепции на интервью и в коде

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

• TypeScript intersection type `A & B` и union type `A | B` соответствуют произведению и копроизведению. Но `A & B` в TS - это «оба свойства», что больше похоже на SET-теоретическое пересечение. Когда intersection type - это произведение, а когда - пересечение? Одно ли это?
• Реализуйте Prism<S, A> для Maybe: Prism<Maybe<A>, A> с операциями preview (Maybe<A> → Option<A>) и review (A → Maybe<A>). Как это связано с копроизведением?
• Профунктор dimap позволяет «контрамапить» вход и «мапить» выход. Чем это отличается от просто Functor (только map)? Приведите пример, где нужен именно dimap, а не map.

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

• plt-01-paradigms
• plt-02-type-systems