Теория категорий
Сопряжённые функторы
Free monad над Set = List. Linux kernel I/O = монада IO в Haskell. NumPy sum = гомоморфизм из свободного моноида. Сопряжённые функторы - самая универсальная структура в математике.
- fold/reduce в Python/Haskell: гомоморфизм из List(S) в моноид M
- Каррирование в JavaScript: Hom(A×B, C) ≅ Hom(A, B→C) - сопряжение Product ⊣ Exponential
Сопряжение: изоморфизм Hom-множеств
Free monad над Set = List. Linux kernel I/O system использует монаду IO в Haskell: одна абстракция, два домена - OS kernel и функциональный язык. Свободная группа над {a, b, c} - это все слова из букв и их инверсий. Понять, почему это так, можно через одну конструкцию: free/forgetful adjunction.
Функтор F: C -> D левоприсоединён к G: D -> C (пишем F - G), если для всех объектов A в C и B в D существует естественный изоморфизм множеств: Hom_D(F(A), B) ≅ Hom_C(A, G(B)). Стрелки из F(A) в B взаимно однозначно соответствуют стрелкам из A в G(B).
Изоморфизм Hom(A x B, C) ≅ Hom(A, B -> C) - это сопряжение каких функторов? Что такое F и G в данном случае?
Free/Forgetful: почему List - это свободный моноид
Свободная конструкция - самый важный пример сопряжения. Забывающий функтор U: Mon -> Set отправляет моноид на его носитель (забывает структуру). Свободный функтор F: Set -> Mon строит свободный моноид над множеством. Изоморфизм Hom_Mon(F(S), M) ≅ Hom_Set(S, U(M)) означает: гомоморфизм из свободного моноида = задание образов генераторов.
Свободный моноид над S - это List(S) со сложением (конкатенацией) и единицей []. Гомоморфизм из List(S) в моноид M задаётся образами элементов S. Это объясняет, почему fold/reduce работает для любого моноида: это в точности применение гомоморфизма.
Monoidal fold в Haskell: `mconcat :: Monoid a => [a] -> a`. Это буквально применение гомоморфизма из свободного моноида List(a) в моноид a. NumPy sum, PyTorch scatter_add, Spark reduce - все реализуют один паттерн: гомоморфизм из свободной структуры.
Почему fold для любого моноида M корректен и единственно определён, если задать образы генераторов? Как это связано с изоморфизмом Hom_Mon(List(S), M) ≅ Hom_Set(S, U(M))?
Сопряжения порождают монады
Каждое сопряжение F - G порождает монаду G.F с единицей eta (единица сопряжения) и умножением G.eps.F, где eps - коединица. Теорема Айленберга-Мура: каждая монада возникает из некоторого сопряжения. Сопряжения фундаментальнее монад.
Curry-Howard соответствие: сопряжение currying соответствует закону экспортации в пропозициональной логике. (A and B => C) эквивалентно (A => (B => C)). Программы = доказательства. Типы = формулы. Сопряжения = логические эквивалентности.
Пять ключевых сопряжений в математике и CS: (1) Free - Forgetful: свободные алгебры. (2) Product - Exponential: каррирование. (3) Colimit - Diagonal: копределы. (4) Diagonal - Limit: пределы. (5) Exists - Substitution - Forall: кванторы в логике.
Как из сопряжения F - G строится монада? Что играет роль eta и mu монады?
Ключевые идеи
- F - G: изоморфизм Hom_D(F(A),B) ≅ Hom_C(A,G(B)), естественный по A и B
- Единица eta: Id -> G.F (вложить) и коединица eps: F.G -> Id (спроецировать) с треугольными тождествами
- Free - Forgetful: свободный моноид = List; fold = применение гомоморфизма
- Product - Exponential: каррирование = сопряжение = закон экспортации (Curry-Howard)
- Каждое сопряжение F - G порождает монаду G.F; все монады возникают из сопряжений
Связанные темы
Сопряжения объединяют монады, пределы и логику.
- Монады — Каждая монада G.F порождается сопряжением F - G
- Пределы и копределы — lim - правый, colim - левый присоединённый к диагональному функтору