рисуем монаду

[thedeemon]

Сегодня в нашем кружке "теоркат для самых маленьких" урок рисования. Будем рисовать монаду. (А то весной кое-кто писал "если монаду нельзя нарисовать, то её нет".)

Для начала нарисуем что-нибудь совсем простое. Палка, палка, огуречик - получился моноид. Моноид состоит из множества (вообще-то необязательно, может быть и штука побольше чем множество), бинарной ассоциативной операции на нем и выделенного элемента, называемого единицей. Бинарная операция берет любые два элемента из этого множества и выдает какой-нибудь один элемент оттуда же.

Она должна быть ассоциативной, т.е. (a*b)*c = a*(b*c):

Тут мы используем нечто вроде фейнмановских диаграмм, где время на рисунке идет снизу-вверх. В самом низу - что было, в самом верху - что получилось, в середине всякие превращения.
Единица моноида - это такой элемент, на который если умножать что угодно слева или справа, получится то, что умножали:

Примеры моноидов: (целые числа, умножение, 1), (целые числа, сложение, 0), (строки, конкатенация, ""), (натуральные числа, максимум, 0) и т.д.

Категория состоит из набора объектов и набора стрелок между ними, функтор отображает одну категорию в другую, сохраняя рисунок стрелок. Если функторы F и G оба отображают категорию C в категорию D, бывает, что можно построить отображение функтора F в функтор G, тоже сохраняющее структуру, такое отображение h называется естественным преобразованием:


Давайте возьмем этот рисунок и применим двойственность Пуанкаре, где k-мерные штуки превращаются в (n-k)-мерные. Возьмем n=2. Категории C и D были нульмерными точками, станут двумерными фигурами. Функторы были одномерными линиями, такими и останутся. Естественное преобразование было двумерной полосой, станет нульмерной точкой. Получим такой вот рисунок, называемый струнной диаграммой:

В такой диаграмме используется вся площадь рисунка. Функторы теперь изображаются не стрелками, а линиями, по разные стороны от которых находятся заливающие пространство рисунка категории, которые этот функтор отображает одну в другую. Что во что отображается определяется направлением. В данном случае слева-направо, в последующих картинках будет справа-налево. Естественное преобразование из одного функтора в другое стало точкой, их соединяющей. Опять же, что во что отображается показано направлением: снизу-вверх.

Что такое монада? Это, во-первых, эндофунктор, т.е. функтор из одной категории в нее же. Назовем его Т. Во-вторых, это пара естественных преобразований μ (от слова мюльтипликейшн) и эта, как ее, в общем, η. Первое превращает Т*Т в Т, второе 1 (identity functor, отображающий категорию саму в себя вообще без изменений) в Т.

Во всяких хаскелях вместо μ (он же join) используют bind (он же >>=), они друг через друга легко выражаются. η в хаскелях известно под именем return.
Конечно, преобразования это не любые, а подчиняющиеся определенным законам. Которые часто изображают в виде требования коммутирования таких вот диаграмм:

Альтернативные пути из точки А в точку Б на таких диаграммах показывают, какие стрелки и их композиции должны быть равны между собой. Например, тут говорится, что неважно, с какой стороны мы к Т добавляем η-й еще один Т, все равно применение к полученному Т² μ дает тот же самый Т.
В данных диаграммах точки означают эндофункторы, а стрелки - естественные преобразования. Подвергнем их той же процедуре дуализации, получим струнные диаграммы:

Теперь естественные преобразования стали жирными точками, а категории - двумерным пространством. Единичный функтор, ничего не делающий, мы обозначим 1, но линию проводить не будем. А теперь сравните эти рисунки с рисунками про законы моноида. Это абсолютно те же самые рисунки, просто с другими обозначениями! Ибо воистину, монады образуют моноид, у которого "множество" - это "множество" эндофункторов в некоторой категории, умножение - их композиция, а единица - единичный функтор (Identity). (Upd: тут я несколько наврал, см. исправления в комментариях.) Классическая цитата "monads are monoids in the category of endofunctors" имеет довольно простой смысл.

Монаду нарисовали, до перемены еще есть время, давайте нарисуем сопряженные функторы. Пусть у нас есть категории C и D и функторы G : C -> D и F : D -> C (теперь это не обязательно эндофункторы, C и D могут быть реально разными категориями).

При определенных условиях эти два функтора называются сопряженными. Условия эти могут быть сформулированы по-разному, например так. Должны существовать естественные преобразования
ε : FG -> 1,
η : 1 -> GF,
называемые counit и unit, такие, что поочередное их применение в разном порядке эквивалентно identity transformation, т.е. композиция F -> FGF -> F равна id, и G -> GFG -> G тоже. Нарисуем ε и η в виде струнных диаграмм:

и изобразим требования к их композиции в виде равенства диаграмм:


Из этих кирпичиков мы можем сложить рисунок побольше:

Тут GFGF применением ε к средней паре превращается в GF. Если мы обозначим композицию GF как Т, то получим преобразование TT -> T, аналогичное монадному μ.
Теперь построим еще больше картинку, и применим interchange rule, позволяющее двигать части картинки туда-сюда, не нарушая ее структуры. Потянув левую точку слияния вверх, а правую вниз, мы получим картинку, где порядок применения преобразований поменялся, но результат остался тем же.

Фактически, мы получили правило ассоциативности μ для T=GF, в точности как на левой картинке про монадные законы и на картинке про ассоциативность бинарной операции в моноиде.

Теперь построим картинку с использованием η и ε.

Cогласно законам сопряженных функторов, левую загогулину GFG можно выпрямить в одну линию G, тогда получим просто композицию GF, т.е. Т. Аналогично, в симметричной картинке можно выпрямить правую загогулину FGF до просто F, чтобы в итоге получилась та же T = GF. Так мы получили картинку, аналогичную правой части картинки про монадные законы, т.е. выполнение свойств единицы, 1 * Т = Т = Т * 1. Таким образом, композиция GF сопряженных функторов дает нам не просто эндофунктор T, а самую настоящую монаду.

При желании струнные диаграммы расширяются в третье измерение, получаются всякие такие доказательства:



Но об этом я вам не расскажу.

На этом все, всем успехов на приближающемся ICFPC!

Comments

[juan-gandhi.livejournal.com]

Отличные картинки!

[maxim.livejournal.com]

Это достойно что бы попасть в wiki-анналы.

[geekyfox.livejournal.com]

Дмитрий, у меня к тебе просьба. Когда в следующий раз соберёшься писать такие вот крутые посты, пожалуйста делай аннаунсмент за сутки-двое, чтобы я взял травы для большей объёмности восприятия.

В этот раз под пивко пошло, надо сказать, неплохо и весьма приятно, но без должной полноты.

Вообще офигенно, чё.

[theiced.livejournal.com]

http://78.47.238.195/lj/md15volume.png

так вот какие они...

[sassa-nf.livejournal.com]

"Ибо воистину, монады образуют моноид, у которого "множество" - это "множество" эндофункторов в некоторой категории, умножение - их композиция, а единица - единичный функтор (Identity). Классическая цитата "monads are monoids in the category of endofunctors" имеет довольно простой смысл."

А про это ещё раз.

1. Монады образуют моноид (один) или монады образуют моноиды (по одному моноиду на монаду)? (ибо инглиш гласит нам, что моноидов много)

2. А умножение = композиция (произвольных эндофункторов) - это каким образом заслуга монад?

3. Тут как-то ещё не ясно, почему умножение - это композиция, если стрелками в категории эндофункторов являются эта, м...

[valentin budaev (from livejournal.com)]

Автор допустил неточность. В категорных моноидах есть два умножения, первое - это *, в случае множеств это обычное декартово произведение множеств, в случае эндофункторов - композиция эндофункторов. А u - это стрелка u: T*T -> T. если * - декартово произведение, то u - обычная математическая бинарная операция, если * - композиция функторов, то u - конкретное естественное преобразование. При этом требуется, чтобы категория относительно * была аналогом обычного теоретико-множественного моноида, то есть сама * ассоциативна и имеет единицу (множество-синглтон либо тождественный функтор для рассматриваемых случаев), такие категории называются моноидальными (если моноидные законы выполняются с точностью до изоморфизма) и строго моноидальными (если законы выполняются точно).

Таким образом, каждая категория с заданным * образует конкретный "теоретико-множественный моноид" (в кавычках, потому что это не совсем точно), а если выбрать в этой категории тройку (T, u, n) получим конкретный моноид в этой категории.

Если это была категория эндофункторов, то каждый такой категорный моноид (тройка (T, u, n)) образует свою монаду (он и называется монадой, по определению).Ну а каждая монада - есть конкретный моноидл, понятное дело.

А образуют монады в целом моноид или нет - вопрос отдельный, если получится выбрать хорошую * - будут образовывать.

[sassa-nf.livejournal.com]

спасибо.

можно ли сказать, что "*" - продукт в категорном смысле, а u - это проекция?

[nivanych.livejournal.com]

1. В каждой моноидальной категории может быть много моноидов. Это ж стрелка A⊗A→A с ассоциативностью и единицей. Соответственно, в (строгой) моноидальной категории эндофункторов (где в качестве ⊗ выступает композиция функторов) может быть много моноидов. То есть, монада=моноид, правда, в определённой моноидальной категории.
Да, неправильно там написано. В роли "множества" конкретной монады-моноида выступает конкретный выбранный эндофунктор.

2. А где сказано, что это заслуга монад?

3. Ещё можно категорию Cat изобразить, как 2-категорию —
1-стрелки — функторы,
2-стрелки — естественные преобразования.
Соответственно, когда выбираешь какой-то объект и все 1-стрелки вокруг него, то получаешь, что каждую 1-эндострелку можно соединить с каждой.
Нетрудной проверкой убеждаемся, что относительно композиции этих 1-эндострелок, мы получаем строгую моноидальную категорию.
И вообще, любая бикатегория с одним объектом будет моноидальной, если мы композицию 1-стрелок предложим в качестве тензорного произведения в нашей новой моноидальной категории. Ну а 2-стрелки изначальной бикатегории в качестве 1-стрелок новой строящейся моноидальной.

[sassa-nf.livejournal.com]

спасибо. я про μ: AxA→A и η: I→A как моноид читал, и даже кажется понял, а тут - нате; решил уточнить на случай если высказанное автором тоже верно, а я не догоняю.

2. ну, было написано, что "а композиция - это умножение", вот и восстало сознание, что не может такого быть - композиция и I есть всегда, а монада - нет.

3. классное объяснение. Нужно будет про 2-категории почитать ещё раз. А то вопрос какой-то был...

[thesz.livejournal.com]

А вот вопрос. Можно ли свести строковые диаграммы и их переписывание к термам и их переписыванию? Где про это можно почитать?

[nivanych.livejournal.com]

Например, Arrow'ы в Haskell родственны моноидальным диаграммам.
Только без resoning'а про равенства.
То есть, можно точно, но где почитать — не знаю.

[churuss.livejournal.com]

классненько
картиночки здоровские

[nivanych.livejournal.com]

Очень хорошо, очень хорошие картинки.
Спасибо, пригодится, буду ссылку давать.
А вещь-то уходит в очень фундаментальное...

> двойственность Пуанкаре

Всё же, тут нужно быть аккуратнее, когда говоришь такие слова.
Но для быстрого туториала сойдёт, наверное.

Моноидальными диаграммами можно изображать как 2-категории, так и моноидальные. Для (lax monoidal) функторов или 2-функторов, уже надо третье измерение. Ну или для 3-категорий достаточно 3-х измерений, но функторы между ними уже так не изобразить. Или как-то с помощью проекции из 4-го измерения... Надо попробовать, как-нибудь, что ли...

Ещё, идеологически это рядом с понятием "распетливания" или "delooping".
Вот как моноидальную категорию представляют в виде бикатегории с одним объектом — говорят, что у нас это стрелки такие хитрые, а не объекты. Ну а обычные стрелки представляют 2-стрелками.
Ну а бикатегории уже как-то изображают ;-)

[thedeemon.livejournal.com]

Про Poincare dual это я за катстерами повторил, тут по сути их лекции пересказ. Сам-то я не настоящий сварщик. :)

[migmit.livejournal.com]

Красивые картинки. А что за лекция, которой пересказ?

[thedeemon.livejournal.com]

http://www.youtube.com/playlist?list=PL50ABC4792BD0A086

[maxim.livejournal.com]

Так шо какие новости с фронта ICFP?

[thedeemon.livejournal.com]

Сперва написал на хаскеле наивный переборщик, он угадал почти 400 программ, но потом стал затыкаться по памяти. Только что закончил перевод его на D, теперь он работает супер быстро и стабильно укладывается в 2-3 мегабайта оперативки. Сейчас пойду спать, а завтра поженю его с запрашивальщиком, буду дальше очки набирать.

А ты участвуешь?

[gineer.livejournal.com]

это все ясно... не ясное, как в програмировании от него может быть польза...

[katresv.livejournal.com]

По моей скудной практике понятие моноид хорошо иллюстрируют перестановки, повороты геометрических фигур. Я бы добавила, что с этим надо "поиграться" некоторое время, сопоставить повороты и перестановки(простые абелевы группы).
>>Примеры моноидов: (целые числа, умножение, 1), (целые числа, сложение, 0), (строки, конкатенация, ""), (натуральные числа, максимум, 0)
Эти примеры нехороши тем, что банальны, мозг на них не останавливается - вопросов не возникает, но затем многие бьются сразу головой о теорему Кэли и либо буксуют, либо теряют интерес к предмету.

Сам пост очень понравился.

[nivanych.livejournal.com]

Речь-то не о классических моноидах, а об их обобщении в странную для большинства математиков сторону.
То есть, ассоциации про "перестановки-повороты" тут в никуда.

> многие бьются сразу головой о теорему Кэли

А чего там биться?
Вроде ж, несложная вещь?
Но красивая, не спорю — в первый раз, оочень восхитила, до сих пор помню!

[http://users.livejournal.com/_winnie/]

> Категория состоит из набора объектов и набора стрелок между ними, функтор отображает одну категорию в другую, сохраняя рисунок стрелок.
Ок, возможно понятно


> отображение функтора F в функтор G, тоже сохраняющее структуру, такое отображение h называется естественным преобразованием:

А что такое отображение между двумя данными функторами? И структура чего сохраняется, какая у функторов структура?

[thedeemon.livejournal.com]

Там довольно занятно оно строится. Естественное преобразование F в G - на самом деле функция из объектов категории С в стрелки категории D: для всякого объекта Х из С функтор F его отобразит в некий F(X) в D, фунткор G - в некоторый G(X) в D, а естественное преобразование h даст нам для Х стрелку из F(X) в G(X), т.е. покажет, как надо F "подправить", чтобы результат получался как у G.

При этом если у нас в С есть стрелка из Х в У, то F ее отобразит в стрелку F(X)->F(Y), G ее отобразит в стрелку G(X)->G(Y), h нам даст стрелки F(X)->G(X) и F(Y)->G(Y), получается, что из F(X) в G(Y) можно попасть двумя путями, такой квадрат возникает. Так вот, он должен коммутировать, т.е. оба пути должны быть эквивалентны, это и есть требование сохранения для h.

[thedeemon.livejournal.com]

И иллюстрация:
Возьмем функтор F = "список", он отображает всякий тип a в [a].
Возьмем функтор G = Identity, он отображает всякий тип a сам в себя.
Возьмем естественное преобразование h = head : F -> G, т.е.
head : [a] -> a
Оно всякому объекту (типу) а сопоставляет стрелку (функцию) из F(a)=[a] в G(a)=a. В агде и идрисе полный его тип будет:
head : {a:Type} -> (List a -> a)
что еще точнее отражает.
Так, для конкретного типа X=Int оно нам даст функцию [Int] -> Int. В данном случае будет брать первый элемент списка, но могут быть и другие ест. преобразования между этими функторами. Собсно, всевозможные чисто полиморфные функции в хаскеле - это естественные преобразования.

[sober-space.livejournal.com]

Ой, извините :)
Конечно читали...