рисуем монаду
Сегодня в нашем кружке "теоркат для самых маленьких" урок рисования. Будем рисовать монаду. (А то весной кое-кто писал "если монаду нельзя нарисовать, то её нет".)
Для начала нарисуем что-нибудь совсем простое. Палка, палка, огуречик - получился моноид. Моноид состоит из множества (вообще-то необязательно, может быть и штука побольше чем множество), бинарной ассоциативной операции на нем и выделенного элемента, называемого единицей. Бинарная операция берет любые два элемента из этого множества и выдает какой-нибудь один элемент оттуда же.
Она должна быть ассоциативной, т.е. (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.
Конечно, преобразования это не любые, а подчиняющиеся определенным законам. Которые часто изображают в виде требования коммутирования таких вот диаграмм:
Альтернативные пути из точки А в точку Б на таких диаграммах показывают, какие стрелки и их композиции должны быть равны между собой. Например, тут говорится, что неважно, с какой стороны мы к Т добавляем η-й еще один Т, все равно применение к полученному Т2 μ дает тот же самый Т.
В данных диаграммах точки означают эндофункторы, а стрелки - естественные преобразования. Подвергнем их той же процедуре дуализации, получим струнные диаграммы:
Теперь естественные преобразования стали жирными точками, а категории - двумерным пространством. Единичный функтор, ничего не делающий, мы обозначим 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!
Для начала нарисуем что-нибудь совсем простое. Палка, палка, огуречик - получился моноид. Моноид состоит из множества (вообще-то необязательно, может быть и штука побольше чем множество), бинарной ассоциативной операции на нем и выделенного элемента, называемого единицей. Бинарная операция берет любые два элемента из этого множества и выдает какой-нибудь один элемент оттуда же.
Она должна быть ассоциативной, т.е. (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.
Конечно, преобразования это не любые, а подчиняющиеся определенным законам. Которые часто изображают в виде требования коммутирования таких вот диаграмм:
Альтернативные пути из точки А в точку Б на таких диаграммах показывают, какие стрелки и их композиции должны быть равны между собой. Например, тут говорится, что неважно, с какой стороны мы к Т добавляем η-й еще один Т, все равно применение к полученному Т2 μ дает тот же самый Т.
В данных диаграммах точки означают эндофункторы, а стрелки - естественные преобразования. Подвергнем их той же процедуре дуализации, получим струнные диаграммы:
Теперь естественные преобразования стали жирными точками, а категории - двумерным пространством. Единичный функтор, ничего не делающий, мы обозначим 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!