Категории типов. Часть 6. Расширения Кана / Хабр

В этот раз мы рассмотрим операции своеобразного «деления функторов». Начнём с обобщения задачи поиска сопряжённых функторов, но потом убедимся, что расширения Кана являются фундаментальной абстракцией, лежащей в основе множества полезных инструментов.

Поверхностный обзор расширений Кана получился весьма объёмным, поэтому в эту статью не вошла техника получения этих конструкций. По той же причине здесь (почти) не упоминается scala-код. Пришлось оставить эти темы на следующий раз.

Оглавление обзора

Hom-типы
Функторы
Естественные преобразования
Монады
Пределы и сопряжения функторов
5½. Сопряжения из монады
Расширения Кана (данная публикация)
Исчисление концов
Построение монад

Содержание

Определения и свойства
Примеры расширений Кана
Коплотность и передача продолжений
- Монада коплотности
- Монада передачи продолжений
Свободная монада
Монадный трансформер коплотности
Дополнительная литература
Промежуточный итог

Определение и свойства

Правые расширения Кана

Пусть у нас есть функтор и нам нужно найти для него такой , чтобы существовало сопряжение $G_F \dashv F$ с естественными преобразованиями

$\begin{eqnarray} \eta:\; Id \rightsquigarrow F \circ G_F,\\ \varepsilon:\; G_F \circ F \rightsquigarrow Id. \end{eqnarray}$

Функтор выглядит обратным к в том смысле, что их композиция позволяет получить тождественный функтор , играющий роль «единицы» для операции композиции, напоминающей «произведение» функторов. Поэтому для встречается другое обозначение: , что делает сопряжение чуть более наглядным:

$\begin{eqnarray} &\varepsilon:\; Id/F \circ F \rightsquigarrow Id,\\ &\eta:\; Id \rightsquigarrow F \circ Id/F;\\ \\ &Id/F \dashv F. \end{eqnarray}$

Конечно же, имеется в виду не привычное деление, которое могло бы получиться, если бы здесь были строгие равенства и операция \circ коммутировала. Сейчас это просто обозначение, в котором искомый функтор сформулирован через два известных, участвующих в естественных преобразованиях сопряжения. Но оно толсто намекает на обобщение, получаемое, если в коединице сопряжения заменить тождественный функтор на произвольный , определённый на той же категории, что и :

Правым расширением Кана функтора $F:\mathcal{C}\rightarrow\mathcal{D}$ вдоль функ��ора $G:\;\mathcal{C}\rightarrow\mathcal{A}$ называется такой функтор $\mathrm{Ran}_GF \equiv F/G:\; \mathcal{A}\rightarrow\mathcal{D}$ вместе с естественным преобразованием $\varepsilon: F/G \circ G \rightsquigarrow F$ , что для любого кандидата $H:\mathcal{A} \rightarrow \mathcal{D}$ с преобразованием $\alpha: H \circ G \rightsquigarrow F$ существует единственное преобразование $u: H \rightsquigarrow F/G$ , такое что $\alpha=\varepsilon \cdot (u \circ Id_G)$ .

Обозначение $\mathrm{Ran}$ происходит от «Right Kan Extension», а преобразование $\varepsilon$ называют коединицей правого расширения Кана. Вертикальная $\cdot$ и горизонтальная $\circ$ композиции естественных преобразований были представлены в обзоре ранее.

Как же можно «расширить» один функтор «вдоль» другого? У математиков вообще очень своеобразное воображение. Но давайте всё же попробуем их хоть немного понять ~~и простить~~.

Перерисуем предыдущую категориальную диаграмму в таком виде:

Функторы и отображают категорию $\mathcal{C}$ в $\mathcal{A}$ и $\mathcal{D}$ . Само это отображение уже как бы «сопоставляет» между собой образы функторов, подкатегории $F\mathcal{C}$ и $G\mathcal{C}$ . Задача функтора — продемонстрировать это сопоставление, «расширив» его с образа $G\mathcal{C}$ на всю категорию $\mathcal{A}$ так, чтобы естественное преобразование $\varepsilon$ явно переводило объекты из $(F/G\,\circ\,G)\mathcal{C}$ в $F\mathcal{C}$ . Получается, что подкатегория $F\mathcal{C}$ как бы «расширяется» до $(F/G)\mathcal{A}$ , внутри которой есть подкатегория $(F/G\,\circ\,G)\mathcal{C}$ , явно сопоставленная с $F\mathcal{C}$ преобразованием $\varepsilon$ … Ну всё же очевидно, да? Впрочем, неважно — главное, что математики делают вид, что такое название вполне соответствует сути.

Свойства правого расширения Кана

Запись правого расширения Кана через инфиксный оператор отражает своего рода «обратность» этой конструкции по отношению к композиции функторов, аналогично делению по отношению к умножению. В частности, для композиции расширений Кана $Ran_H \circ Ran_G$ справедлива привычная алгебраическая формула:

$(F/G)/H \cong F/(H \circ G).$

Обозначение $\mathrm{Ran}_GF$ является более стандартным. В этом случае $\mathrm{Ran}_G$ сам выступает в роли функтора, действующего между категориями функторов. Если $G:\mathcal{C}\rightarrow\mathcal{A}$ , то для любой категории $\mathcal{D}$ получаем $\mathrm{Ran}_G:\mathcal{D}^\mathcal{C}\rightarrow\mathcal{D}^\mathcal{A}$ . Любопытно, что этот функтор оказывается сопряжённым справа к фун��тору предкомпозиции функторов $\_ \circ G: \mathcal{D}^\mathcal{C}\rightarrow\mathcal{D}^\mathcal{A}$ (где прочерк обозначает место для аргумента-функтора):

$\_ \circ G \dashv \mathrm{Ran}_G.$

Действительно, для любого $H:\mathcal{A}\rightarrow\mathcal{D}$ выпоняется следующий изоморфизм:

$\mathrm{Hom}_{\mathcal{D}^\mathcal{C}}(H \circ G,\, F) \cong \mathrm{Hom}_{\mathcal{D}^\mathcal{A}}(H,\, \mathrm{Ran}_G F).$

Слева здесь морфизмы в категории функторов $\mathcal{D}^\mathcal{C}$ — совокупность естественных преобразований $\alpha: H \circ G \rightsquigarrow F$ , каждое из которых вместе с функтором образует кандидата в правое расширение Кана. Справа же — универсальный морфизм $u: H \rightsquigarrow \mathrm{Ran}_GF$ для этого кандидата. Изоморфизм просто говорит о том, что каждому кандидату взаимно однозначно соответствует единственный универсальный морфизм. Коединица такого сопряжения $\varepsilon_F: (F / G) \circ G \rightsquigarrow F$ соответствует коединице расширения Кана, а единица имеет вид $\eta_F: F \rightsquigarrow (F \circ G) / G$ .

Ранее в предыдущей части обзора мы разбирали сопряжение эндофункторов в категории типов Writer[S] ⊣ Reader[S]. Любопытно, что для него получается внешне похожий hom-изоморфизм: $\mathrm{Hom}(A \times S, B) \cong \mathrm{Hom}(A, B^S)$ . Произведение объектов аналогично (с некоторой натяжкой) композиции функторов, но если первой операции противопоставляется экспоненциал, то во втором случае мы получили что-то вроде деления! Как могут быть связаны экспоненциал и деление?

Эту связь проще понять, сравнив алгебраическое равенство $B/A \times A = B$ и функцию оценки $eval:\; (A \to B) \times A \to B$ . В обоих случаях справа имеем , а слева — произведения чего-то на . Если в одном случае в произведении присутствует дробь , то во втором — экспоненциал $A \to B \equiv B^A$ , который является решением задачи «что в сочетании с позволяет получить ?». Такое неожиданное сопоставление «деления» с «экспоненциалом» обусловлено тем, что в теории категорий так или иначе все вычисления сводятся к манипулированию hom-объектами (в теории типов — функциями). Мы ещё увидим это в следующей части обзора.

Левые расширения Кана

Мы пришли к правому расширению Кана, обобщив задачу поиска левого сопряжения (как ни парадоксально)). Если же бы мы начали с поиска правого расширения, то, ожидаемо, получили бы левое расширение Кана:

Левым расширением Кана функтора $F:\mathcal{C}\rightarrow\mathcal{D}$ вдоль функтора $G:\;\mathcal{C}\rightarrow\mathcal{A}$ называется такой функтор $\mathrm{Lan}_GF:\; \mathcal{A}\rightarrow\mathcal{D}$ вместе с естественным преобразованием $\eta: F \rightsquigarrow \mathrm{Lan}_GF \circ G$ , что для любого кандидата $H:\mathcal{A} \rightarrow \mathcal{D}$ с преобразованием $\alpha: F \rightsquigarrow H \circ G$ существует единственное преобразование $u: \mathrm{Lan}_GF \rightsquigarrow H$ , такое что $\alpha= (u \circ Id_G) \cdot \eta$ .
Обозначение \mathrm{Lan} происходит от «Left Kan Extension», а преобразование $\eta$ называют единицей левого расширения Кана.

В данном обзоре наравне с общепринятым будет использоваться нестандартное обозначение $G \backslash F \equiv \mathrm{Lan}_GF$ . Функтор, который мы факторизуем, располагается как бы над чертой, а через который факторизуем — под ней. Такое обозначение «левого деления функторов» отражает дуализм по отношению к «правому делению» .

По аналогии с $\mathrm{Ran}_G$ , универсальное свойство для $\mathrm{Lan}_G$ образует похожее сопряжение с функтором предкомпозиции, что даёт сопряжённую тройку:

$\mathsf{Lan}_G \dashv (\_ \circ G) \dashv \mathsf{Ran}_G.$

Для левых расширений Кана работает похожее правило композиции: $Lan_H (Lan_G F) \cong Lan_{H \circ G} F$ , или в других обозначениях

$H\backslash(G\backslash F) = (H \circ G)\backslash F.$

Подъёмы Кана

Расширения Кана строятся для функторов, исходящих из одной категории. Но можно пойти и другим путём — рассматривать функторы, сходящиеся в одну и ту же категорию. Тогда получатся ещё два способа факторизации одного функтора по другому. Эти конструкции называются подъёмами Кана $\mathrm{Lift}$ и $\mathrm{Rift}$ . В отличие от расширений Кана, они образуют сопряжённую тройку вокруг посткомпозиции:

$\mathrm{Lift}\, G \dashv (G \circ \_) \dashv \mathrm{Rift}\, G.$

Подъёмы Кана обладают свойствами, аналогичными расширениям, и они имеют те же основания называться «делением функторов». Так что в сумме мы имеем целых четыре различные операции, «обратные» композиции функторов. И это одна из причин, почему инфиксный оператор / не часто используется в качестве обозначения правого расширения Кана.

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

Давайте теперь посмотрим на конкретные примеры как левых, так и правых расширений Кана.

Примеры расширений Кана

Сопряжения

Ранее уже были намёки, но теперь скажем прямо: если для функтора $F:\, \mathcal{C}\rightarrow\mathcal{D}$ существуют левое/правое сопряжение, то это будут (с точностью до изоморфизма) правое/левое расширение Кана тождественного функтора $Id:\mathcal{C}\rightarrow\mathcal{C}$ вдоль :

$\begin{eqnarray} {Id} / F \dashv F \dashv F \backslash {Id}. \end{eqnarray}$

В предыдущей части обзора было показано, как сопряжённые тройки порождают монады и комонады. Представленная тройка интересна тем, что она параметризована единственным функтором — он один порождает целую россыпь (ко)монад:

монады: $F \circ (Id/F):\;\mathcal{D}\rightarrow\mathcal{D}$ и $(F \backslash Id) \circ F:\;\mathcal{C}\rightarrow\mathcal{C}$ ;
комонады: $(Id/F) \circ F:\;\mathcal{C}\rightarrow\mathcal{C}$ и $F \circ (F \backslash Id):\; \mathcal{D}\rightarrow\mathcal{D}$ .

(Ко)пределы

Давайте вспомним, как устроены (ко)пределы функторов. Для некоторого (не для каждого) функтора $F:\mathcal{C} \rightarrow \mathcal{D}$ существуют такие объекты $\mathrm{(Co)Lim}\, F: \mathcal{D}$ , которые в некотором смысле наилучшим образом представляют этот самый функтор. Такой объект, вместе с семейством морфизмов, индексированных объектами $c:\mathcal{C}$ , образуют универсальный (ко)конус — естественное преобразование между заданным функтором и константным $\Delta_{\mathrm{(Co)Lim}\,F}$ .

Константный функтор $\Delta_d: \mathcal{C} \rightarrow \mathcal{D}$ сочетает в себе две операции — полное «забывание» всей структуры категории $\mathcal{C}$ и выбор конкретного объекта $d: \mathcal{D}$ . Удобно факторизовать диагональный функтор на два вспомогательных — один будет отвечать за «схлопывание» исходной категории в категорию , состоящую из единственного объекта и его тождественного морфизма, а другой функтор будет отображать в $\mathcal{D}$ , выбирая там нужный объект :

$\begin{eqnarray} \Delta_d &:& \mathcal{C} \rightarrow \mathcal{D} = d\, \circ\, !,\; \text{где}\\ !&:& \mathcal{C} \rightarrow 1,\\ d&:& 1 \rightarrow \mathcal{D}. \end{eqnarray}$

Категория является терминальным объектом в категории категорий. Функтор является его универсальным морфизмом, единственным образом «забывающим» структуру исходной категории, переводя все её морфизмы в тождественный для единственного объекта. Эта ситуация аналогична той, что мы рассматривали раньше в категории типов — тип Unit является её терминальным объектом, так как существует единственный способ (функция) привести к нему любой другой тип.

Любой функтор, исходящий из , моделирует её в целевой категории , то есть, по сути, выбирает из неё единственный объект. Категория таких функторов изоморфна дискретной подкатегории, построенной на тех же объектах, что и . Поэтому часто для простоты эти функторы обозначают также, как и объекты $d: 1 \rightarrow \mathcal{D}$ .

Получается следующая диаграмма в категории категорий:

Функтор факторизуется через посредством «наилучших» $\mathrm{Colim}_F$ и $\mathrm{Lim}_F$ , что отсылает нас к расширениям Кана.

Действительно, несложно убедиться, что

$\begin{eqnarray} \mathrm{Lim}\, F &\cong& F / !,\\ \mathrm{Colim}\, F &\cong& ! \backslash F. \end{eqnarray}$

Другими словами, если (ко)предел функтора существует, то соответствующий «выбирающий функтор» будет изоморфен левому/правому расширению Кана вдоль .

Представления Йонеды

Ранее мы видели расширения функтора F вдоль себя и тождественного вдоль F. Для полноты картины рассмотрим расширение функтора вдоль тождественного.

Эти расширения Кана соответствуют так называемым представлениям Йонеды:

$\begin{eqnarray} &&よ &=& \mathrm{Ran}_{Id},\\ &&よ^{op} &=& \mathrm{Lan}_{Id}. \end{eqnarray}$

Трудности перевода

Японский математик Нобуо Йонеда (написание через «йо» уже устоялось) доказал в теории категорий очень важную лемму, и мы ещё рассмотрим её позднее. Саундерс Маклейн, один из основателей теории категорий, предложил назвать эту лемму именем автора. То же имя получили специфичный для леммы функтор $\mathcal{C} \to \mathrm{Set}^{\mathcal{C}}$ (вложение Йонеды), а также рассмотренные выше представления функторов.

Для этих конструкций иногда используют обозначения $\mathcal{Y}$ или просто $\operatorname{Yoneda}$ , но в одной работе 2015 года предложили более короткое обозначение $\operatorname{よ}$ — букву японской азбуки хирагана, читающуюся как «ё», первый слог фамилии Йонеды.

Японские фамилии обычно записывают иероглифами, которые могут иметь разное прочтение, и японцы пользуются хираганой, чтобы пояснять, как правильно читать их фамилии. Оригинальная запись фамилии Йонеды состоит из двух иероглифов: «米田», где «米» имеет самостоятельное значение «рис» и читается как [коме]. Поэтому использовать такой символ в качестве математического обозначения было бы не лучшей идеей.

Авторы той статьи обосновывали отказ от символа 米 как-то так: «в нём слишком много черт, и неудобно записывать на доске»… В данном же обзоре символ $\operatorname{よ}$ выбран ещё и потому, что его произношение «Ё» несёт особую энергетику, которая призвана помочь программистам в усвоении основ теории категорий)).

Кстати, обычно этот символ используют для вложения Йонеды, но здесь им обозначены именно представления Йонеды, так как они более важны в программировании.

Интересной особенностью представлений Йонеды является то, что они изоморфны исходным функторам:

$\mathop{よ} F \cong F \cong \mathop{よ^{op}} F.$

Действительно, возьмём к примеру представление ко-Йонеды $\mathop{よ^{op}}F = Id \backslash F$ . Единица этого расширения Кана даёт одну ветвь изоморфизма $\eta: F \rightsquigarrow \mathop{よ^{op}}F$ . Обратную ветвь мы получим как универсальный морфизм $u_F: \mathop{よ^{op}}F \rightsquigarrow F$ , если в качестве кандидата выберем с преобразованием $\alpha= u_F \cdot \eta=Id_F$ . Универсальный морфизм буквально является обратным к единице $\eta$ и при этом он однозначно фиксирован выбором кандидата. Для представления Йонеды $\mathop{よ}F = F / Id$ результат будет аналогичным.

Казалось бы, какая может быть польза от изоморфных функторов? Секрет в том, что представления позволяют оптимизировать цепочки простых преобразований внутри «контейнера» $F: \mathcal{C} \to \mathcal{D}$ . А именно, если последовательность морфизмов из категории $\mathcal{C}$ по шагам переносится представлением Йонеды функтора в $\mathcal{D}$ , то, (внезапно!) сам функтор при этом не задействуется! Представление на каждом шаге комбинирует преобразования в одно действие, тогда как $よ^{op}$ запоминает их в своеобразном «списке». К сожалению, не нашёл способа продемонстрировать эту оптимизацию, не вникая в устройство представлений Йонеды и расширений Кана. Но мы обязательно сделаем это в продолжении обзора.

В обоих случаях реальное использование функтора происходит лишь в момент «распаковки» представления посредством изоморфизма. Наиболее принципиальное различие между представлениями заключается лишь в том, на каком этапе требуется предоставить доказательства функториальности — при переходе к представлению, или при возвращении обратно.

Представление ко-Йонеды также часто называют свободным функтором. Дело в том, что в общем случае для отображения $F: \mathcal{C} \to \mathcal{D}$ , переводящего морфизмы одной категории в другую, у нас могут отсутствовать «свидетельства» функториальности. Но даже в этом случае мы можем построить для представление ко-Йонеды, которое будет полноценным функтором! Поэтому и говорят, что $\mathop{よ^{op}}F$ является функтором, свободным от наличия функториальности самого . Она может понадобиться лишь для «распаковки» $\mathop{よ^{op}}F \rightsquigarrow F$ , но и тут зачастую есть возможность выкрутиться, если получится преобразовать в какой-нибудь настоящий функтор .

Коплотность и передача продолжений

Монада коплотности

Не для каждого функтора могут существовать левое и правое сопряжения. В таких случаях расширения Кана и $F \backslash Id$ можно рассматривать как «наилучшие попытки» построить сопряжения. Если же для функтора $F:\, \mathcal{C}\rightarrow\mathcal{D}$ сопряжения существуют, то справедливыми оказываются следующие изоморфизмы:

$\begin{eqnarray} F \circ (Id/F) \cong F/F,\\ F \circ (F \backslash Id) \cong F \backslash F. \end{eqnarray}$

Соотношения кажутся очевидными со школы, но ввиду не совсем обычных операций «деления функторов», можно считать, что они получились совершенно случайно)).

К примеру, рассмотрим первый изоморфизм, представленный двумя встречными естественными преобразованиями:

$\begin{eqnarray} \varphi:\;& F \circ (Id / F) &\rightsquigarrow&& F/F,\\ \psi:\;& F/F &\rightsquigarrow&& F \circ (Id / F).\\ \end{eqnarray}$

Они должны фиксироваться известными преобразованиями сопряжения, а также коединицей расширения Кана $\varepsilon_{\mathrm{Ran}}$ :

$\begin{eqnarray} \varepsilon_\dashv:\;& (Id / F) \circ F &\rightsquigarrow Id, \\ \eta_\dashv:\;& Id &\rightsquigarrow F \circ (Id / F), \\ \varepsilon_{\mathrm{Ran}}:\;& (F / F) \circ F &\rightsquigarrow F. \end{eqnarray}$

С их помощью одна ветвь изоморфизма выражается так:

$\psi = (\varepsilon_{\mathrm{Ran}} \circ Id_{Id/F}) \cdot (Id_{F/F} \circ \eta_\dashv).$

А вот для явного выражения $\varphi$ данных преобразований недостаточно. Тут нас выручит универсальный морфизм расширения Кана $u_G:\; G \rightsquigarrow F/F$ , взаимно однозначно соответствующий преобразованию $\alpha_G: F \circ G \rightsquigarrow F$ , заданному для произвольного кандидата $G: \mathcal{D} \rightarrow \mathcal{D}$ . Выберем в качестве кандидата тождественный функтор в категории $\mathcal{D}$ с тождественным преобразованием $\alpha_{Id}=Id_F: F \rightsquigarrow F$ . Для такого кандидата у нас будет универсальный морфизм вида

$u_{Id} = Id \rightsquigarrow F/F.$

Он поможет нам явно выписать другую ветвь искомого изоморфизма:

$\varphi = (Id_{F/F} \circ \varepsilon_\dashv) \cdot (u_{Id} \circ Id_{F \circ (Id/F)}).$

Тут можно заметить подвох — утверждается, что у нас уже есть преобразование $u_{Id}$ , однозначно фиксированное известными $\varepsilon_{\mathrm{Ran}}$ и $\alpha_{Id}$ через универсальное свойство. Однако $u_{Id}$ определяется как решение уравнения $\alpha_{Id}=\varepsilon_{\mathrm{Ran}} \cdot (u_{Id} \circ Id_F)$ , и для него просто нет явного выражения в виде композиции естественных преобразований! Мы, конечно, могли бы попробовать ввести что-то вроде операции «деления естественных преобразований», но тут используется другой подход, и мы рассмотрим его в другой раз. Пока же достаточно того, что нам удалось продемонстрировать корректность изоморфизма $F \circ (Id/F) \cong F/F$ .

Так зачем же нам заморачиваться с таким изоморфизмом и функтором ? Сопряжение даёт нам монаду для $F \circ (Id/F)$ , но фокус в том, что образует монаду даже тогда, когда функтор вообще не имеет левого сопряжения! Правое расширение Кана функтора вдоль самого себя называется монадой коплотности функтора :

$\mathrm{Codens}\, F \equiv \mathrm{Ran}_F F.$

Преобразования монады можно получить, воспользовавшись знакомым трюком, основанном на эксплуатации универсального свойства расширения Кана для конкретных кандидатов. Полученное ранее преобразование $u_{Id} = Id \rightsquigarrow F/F$ даёт «запаковку» для нашей монады. Если же в качестве кандидата выберем $F/F \circ F/F$ с преобразованием $\alpha: F/F \circ F/F \circ F \rightsquigarrow F = \varepsilon_{\mathrm{Ran}} \cdot (Id_{F/F} \circ \varepsilon_{\mathrm{Ran}})$ , то ему будет взаимно однозначно соответствовать универсальный морфизм $u: F/F \circ F/F \rightsquigarrow F/F$ , по счастливой случайности отвечающий как раз за «разматрёшивание» монады.

Универсальное свойство монады коплотности обладает ещё одной замечательной особенностью. Дело в том, что в преобразовании $\alpha: (F/F)^n \circ F \rightsquigarrow F$ для кандидатов вида можно поменять левую ассоциативность композиции на правую:

$\begin{eqnarray} \alpha &=& \varepsilon_{Ran} \cdot (Id_{F/F} \circ (\varepsilon_{Ran} \cdot (Id_{F/F} \circ (\varepsilon_{Ran} \cdot \ldots))))\\ &=& \varepsilon_{Ran} \cdot (Id_{F/F} \circ \varepsilon_{Ran}) \cdot (Id_{(F/F)^2} \circ \varepsilon_{Ran}) \cdot \ldots \end{eqnarray}$

Здесь учтено, что $Id^n_{F/F} \equiv Id_{(F/F)^n}$ . Коединица $\varepsilon_{\mathrm{Ran}}:\; (F / F) \circ F \rightsquigarrow F$ по сути отвечает за «распаковку» функтора , а преобразование $\alpha$ является композицией таких распаковок.

Кандидату с таким преобразованием $\alpha$ соответствует универсальный морфизм $u: (F/F)^n \rightsquigarrow F/F$ , отвечающий за многократное монадное «разматрёшивание». Его устройство мы изучим в другой раз, но, по аналогии с $\alpha$ , очевидно, что каждая его компонента — это просто композиция обычных ~~функций~~ морфизмов! Универсальное свойство меняет лево-ассоциативную композицию, используемую при построении, на право-ассоциативную, оптимизированную для вычислений. Это позволяет разматрёшивать глубокую вложенность $(F/F)^na \stackrel{u_a}\to (F/F)a$ за один проход, просто применяя преобразования справа налево.

В программировании монада коплотности даёт мощную оптимизацию вычислений цепочек функций с эффектами. Она позволяет «схлопывать» произвольное количество вызовов flatMap в единую функциональную композицию, сохраняя при этом исходный контекст F[A]. Если F[_] — это тяжеловесная рекурсивная структура (будь то список, дерево SQL-запроса или свободная монада), коплотность превращает квадратичную сложность выполнения n преобразований в линейную , делая доступ к каждому следующему шагу вычисления мгновенным .

Аналогично доказывается изоморфизм $F \circ (F \backslash Id) \cong F \backslash F$ . Левое расширение Кана функтора вдоль самого себя образует комонаду плотности $\mathrm{Dens}\, F \equiv F \backslash F$ , и её существование не зависит от наличия правого сопряжения к .

(Ко)монады в категории $\mathcal{C}$ , порождённые сопряжённой тройкой, построенной вокруг функтора $F:\mathcal{C} \to \mathcal{D}$ , также иногда описывают с позиции «плотности»:

$\begin{eqnarray} (F \backslash Id) \circ F &\;\;-\;& \text{монада плотности;}\\ (F / Id) \circ F &\;\;-\;& \text{комонада коплотности.} \end{eqnarray}$

Они имеют больше отношения к упомянутым ранее подъёмами Кана, и упоминаются редко.

Про «плотность»

Концепция плотности позаимствована из топологии. Считается, что множество плотно в (как рациональные числа в вещественных), если любая точка $d \in D$ является пределом последовательности из . Теория категорий обобщает это понятие: функтор $F:\mathcal{C}\to\mathcal{D}$ называется (ко)плотным, если для каждого $d:\mathcal{D}$ в образе найдётся такая диаграмма, что будет её (ко)пределом.

Для плотного функтора выполняется условие $F \backslash F \cong Id$ , а для коплотного — $F / F \cong Id$ . Если эти расширения Кана не изоморфны тождественному эндофунктору, значит функтор отображает исходную категорию «не (ко)плотно» — либо в исходной категории не достаточно данных, либо сам функтор слишком «забывчивый». Плотные функторы позволяют «воссоздать» из своего образа все объекты категории $\mathcal{D}$ .

Коплотные функторы содержат в своём образе достаточно диаграмм, чтобы «детектировать» все объекты в $\mathcal{D}$ , различить их только на основе морфизмов из образа.

И плотные, и коплотные функторы отвечают за своеобразное «кодирование» целой категории лишь малой её частью, но делают они это по-разному, дуально. Естественно, большинство функторов не обладают ни тем, ни другим свойством, но есть и такие, которые являются и плотными и коплотными одновременно. Например, это изоморфизмы категорий, или отображения в скелет категории (содержащий лишь по одному объекту для каждого изоморфизма в категории).

Монада передачи продолжений

Итак, представление Йонеды позволяет оптимизировать цепочку чистых вычислений под функтором, тогда как монада коплотности специализируется на оптимизации вычислений с эффектами. Оказывается, мы можем объединить эти оптимизации, построив монаду передачи продолжений:

$\mathrm{Cont}\, F = \mathrm{Ran}_{よ_F}F = F/(F/Id).$

Полученная монада изоморфна коплотности $\mathrm{Cont}\, F \cong \mathrm{Codens}\, F$ , но именно в этом виде она более оптимизирована. Для обратного преобразования $\mathrm{Cont}\, F$ в требуется передать функцию с эффектом , продолжающую вычисления с «запакованным» значением (мы увидим, как это работает, в продолжении обзора). Отсюда и происходит название монады.

Данная конструкция лежит в основе особой техники программирования — стиля передачи продолжений (Continuation Passing Style). Эта техника встроена в компиляторы многих языков программирования и применяется в различных библиотеках Scala, в том числе в новомодном «direct style», активно продвигаемом Мартином Одерски.

Свободная монада

Формулировка через левое расширение Кана

Само устройство свободной монады функтора мы рассмотрим в продолжении обзора. Сейчас просто примем, что она выражается через левое расширение Кана

$\mathrm{Free}\, F = U \backslash U,$

где $U: \mathcal{Alg}_F \to \mathcal{C}$ — забывающий функтор из категории F-алгебр. Объектами этой категории являются пары $(c:\mathcal{C},\, h: Fc \to c): \mathcal{Alg}_F$ , а морфизмы между и представляют собой функции $f: a \to b$ , такие что $f \circ g = h \circ Ff$ (гомоморфизмы алгебр функтора). Действие забывающего функтора на морфизмы тривиально, а из объектов он просто выбрасывает второй элемент пары. Поэтому можно считать, что для любого автоматически задан такой забывающий функтор.

Тут стоит отметить два очень важных факта.

Во-первых, категория алгебр функтора сильно отличается от категории алгебр монады, рассмотренной ранее в обзоре. В первой меньше ограничений, а значит, больше объектов и морфизмов. Мы разберём этот нюанс подробнее в другой раз, но сейчас важно просто не спутать эти категории.

Во-вторых, как мы уже видели раньше, левое расширение Кана $U \backslash U: \mathcal{C} \to \mathcal{C}$ образует комонаду плотности забывающего функтора $U: \mathcal{Alg}_F \to \mathcal{C}$ . Но магическим образом оно же является и свободной монадой для эндофунктора $F: \mathcal{C} \to \mathcal{C}$ !

В отличие от монады коплотности, здесь мы не получаем изоморфизма с исходным функтором: $\mathrm{Free}\,F \ncong F$ . Однако универсальное свойство расширения Кана даёт нам естественное преобразование $u: F \rightsquigarrow \mathrm{Free}\,F$ и преобразование морфизмов $lift(f: a \to Fb): a \to \mathrm{Free}\,F\,b = u_b \circ f$ , которое позволяет строить монадические композиции F-эффективных функций для абсолютно любого функтора :

$\begin{eqnarray} f&:& a \to Fb,\\ g&:& b \to Fc,\\ \tilde{f} &=& lift(f)&:& a \to \mathrm{Free}\,F\,b,\\ \tilde{g} &=& lift(g)&:& b \to \mathrm{Free}\,F\,c,\\ \tilde{h} &=& \tilde{g} \circ \tilde{f}&:& a \to \mathrm{Free}\,F\,c,\\ \end{eqnarray}$

Функция $\tilde{h}$ является программой, составленной из F-эффектных шагов, «поднятых в мир Free». Исполнение такой программы осуществляется с помощью преобразования $foldMap: (F \rightsquigarrow G) \to (\mathrm{Free}\,F \rightsquigarrow G)$ для заданной монады с дальнейшей «распаковкой» этой монады.

Другие представления

Существуют и другие представления свободной монады. Например, её можно выразить в виде копредела функтора $P_F: \mathbb{N} \to \mathcal{C}^\mathcal{C} = \forall{n: \mathbb{N}}.\; F^n$ ( $\mathbb{N}$ — натуральные числа, включающие ). Но сейчас мы не будем погружаться в эти детали. Достаточно только иметь в виду, что копредел также выражается через левое расширение Кана и свободная монада в таком представлении выглядит так: $\mathrm{Free}\,F =\, ! \backslash P_F$ .

Более свободная монада

Свободная монада эндофунктора $F: \mathcal{C} \to \mathcal{C}$ «освобождает» нас от необходимости предоставлять монадные преобразования для этого функтора. Ранее же мы видели, что представление ко-Йонеды «освобождает» нас даже от функториальности . Естественно, мы можем объединить две эти конструкции, получив более свободную монаду:

$\mathrm{Freer}\, F = \tilde{U} \backslash \tilde{U},$

где $\tilde{U}: \mathcal{Alg}_{よ^{op}F} \to \mathcal{C}$ — забывающий функтор из категории алгебр уже для $よ^{op}F$ .

Более свободная монада позволяет строить пути вычислений из шагов вида $a \to Fb$ даже если не является функтором (нет свидетельства функториальности)! Выполнение вычислений производится с помощью такого же (только преобразования от «не-функтора» уже не могут называться «естественными»).

Перечисленные особенности лежат в основе специальной техники программирования, собирающей «программу-как-данные» из абстрактных контейнеров (GADT), описывающих бизнес-операции. В конце такая программа «сворачивается» с использованием интерпретаторов этих контейнеров в какой-нибудь IO.

Оптимизированная свободная монада

И конечно же, свободную монаду можно оптимизировать, обернув её в монаду продолжения:

$\mathrm{FastFree}\, F = \mathrm{Cont}\, \mathrm{Freer}\, F.$

Эта идея стала популярной благодаря работам Олега Киселёва:

Reflection without Remorse (2014),
Freer Monads, More Extensible Effects (2015).

В языке Scala оптимизированная свободная монада реализована в нескольких библиотеках, но немного по-разному.

В библиотеке Scalaz монада продолжений реализована явно, но тип Free[F[_], A] воплощает конструкцию $\mathrm{Cont}\, \mathrm{Free}$ для существующих функторов (оптимизация продолжениями обеспечивается слагаемым Gosub <: Free). Если нужно «освободить не-функтор», то для этого используется тип FreeC[F[_], A], в точности соответствующий определённому выше $\mathrm{FastFree}$ .
В библиотеке Cats представлен аналогичный тип Free[F[_], A], который ближе к простому $\mathrm{Freer}$ . Но «под капотом» шаги преобразований переассоциируются методом step внутри foldMap (или run), что и отсылает к монаде продолжений.
В библиотеке Eff реализованы основные идеи Киселёва. Контейнер Eff[FT, A] устроен сложнее, чем обычная свободная монада (FT является неким значком, соответствующим композиции различных F[_]), и это даёт очень интересные возможности по комбинированию эффектов. Но концептуально, это воплощение всё того же $\mathrm{FastFree}$ .
Также в библиотеках встречается контейнер Eval[_], который представляет собой свободную монаду, построенную над Id.

Таким образом, конструкции Free, которые современные библиотеки предоставляют в качестве свободной монады, реализуют сложную абстракцию, собранную из множества расширений Кана.

Монадный трансформер коплотности

Пусть у нас есть монада $(T: \mathcal{C} \to \mathcal{C},\, \eta^T,\, \mu^T)$ и функтор $F: \mathcal{C} \to \mathcal{D}$ . Давайте рассмотрим такое расширение Кана: $(F \circ T)/F$ . Его коединицей будет $\varepsilon: (F \circ T)/F \circ F \rightsquigarrow F \circ T$ . Оказывается, что $(F \circ T)/F$ образует новую монаду $(S: \mathcal{D} \to \mathcal{D},\, \eta,\, \mu)$ .

Её естественные преобразования, а также специальная операция «подъёма» $\lambda: F \circ T \rightsquigarrow S$ однозначно фиксируются следующими уравнениями, получаемыми благодаря универсальным морфизмам для разных кандидатов :

$\begin{eqnarray} \varepsilon \cdot (\eta \circ Id_F) &=& Id_F \circ \eta^T,\\ \varepsilon \cdot (\mu \circ Id_F) &=& (Id_F \circ \mu^T) \cdot (\varepsilon \circ Id_T) \cdot (Id_S \circ \varepsilon),\\ \varepsilon \cdot (\lambda \circ Id_F) &=& Id_{F \circ T}. \end{eqnarray}$

Такое расширение Кана трансформирует монаду T вдоль функтора F из категории $\mathcal{C}$ в $\mathcal{D}$ !

Стоп, не всё так просто. Монада получается вовсе не для любых и . Существуют такие частные случаи , при которых мы получим монаду для любого , но это не особо интересно. Самое важное ограничение накладывается на функтор — для него должен существовать лево сопряжённый $L \dashv F$ , тогда мы сможем трансформировать вдоль него любую монаду . По этой причине часто говорят о построении монадного трансформера (устоявшееся название) вдоль функтора :

$\mathrm{Trans}\, F: \mathcal{C}^\mathcal{C} \to \mathcal{D}^\mathcal{D} = \mathrm{Ran}_F\, (\_ \circ F).$

Конечно же, здесь подразумевается не только трансформация самих эндофункторов, но и естественных преобразований соответствующих монад.

В программировании мы обычно имеем дело с эндофункторами в одной и той же категории типов $\star$ , так что монадные трансформеры иногда рассматриваются как легальный способ композиции монад. Благодаря «подъёму» $\lambda$ и «спуску» $\varepsilon$ , расширение Кана $(F \circ G)/F$ порождает монаду, которую часто ассоциируют именно с композицией $F \circ G$ . Но в данном случае речь идёт скорее не о композиции, а об «индуцировании» новой монады из исходной . Если у эндофунктора есть свои монадные возможности, то они не задействуются, а вместо них срабатывает механика коплотности.

Важный момент: обычно программисты имеют дело с трансформерами вида FT[G, ], соответствующими функторам G[F[]]. Такой трансформер жёстко привязан к структуре внутренней монады композиции. В Scala-библиотеках представлены скромные наборы таких трансформеров для наиболее востребованных монад, но нет способов построить универсальный трансформер, работающий для любой внутренней монады F.

Полученный здесь монадный трансформер коплотности работает иначе. В отличие от привычных трансформеров, он надстраивается над внешним функтором композиции $F \circ G$ . Кроме того, в программировании устраняется неудобное ограничение расширения Кана. В декартово замкнутой категории типов присутствуют типы любых функций. Расширения Кана здесь будут не просто поточечными, но сильными, что выражается в программировании посредством полиморфных функций высокого порядка. Это снимает ограничение на представимость функтора (на наличие левого сопряжения), что позволяет строить монады действительно для любых и !

Дополнительно, структура коплотности даёт рассмотренную ранее оптимизацию цепочки вычислений в контексте этой монады.

Дополнительная литература

Из Кафе Программирования Бартоша Милевски
Публикации из блога Comonads Эдварда Кметта
Публикации из блога String Diagrams Дэна Марсдена:
Статья Тома Лейнстера The Yoneda Lemma: What's It All About (pdf)

Промежуточный итог

Композицию функторов часто ассоциируют с понятием «умножения», а расширения Кана иногда трактуют как своеобразные операции «деления функторов». Именно по этой причине в данной публикации чаще используются обозначения расширений Кана в виде дробей. Но важно понимать, что, в отличие от школьной алгебры, здесь «умножение» не перестановочно, а «дроби» далеко не всегда удаётся упростить. И вообще, мы имеем не одну, а сразу две обратные операции — левое $\mathrm{Lan}$ и правое $\mathrm{Ran}$ расширения Кана (плюс ещё пара редко используемых подъёмов Кана).

Расширения Кана дополняют операцию композиции функторов, что позволяет решать обратные задачи — вычислять функторы, удовлетворяющие заданным композиционным уравнениям. Подобные уравнения возникают, например, когда требуется вычислить (ко)предел функтора, или же его левое/правое сопряжение.

Большое значение имеют конструкции (ко)Йонеды и (ко)плотности. Первые представляют собой расширения заданного функтора вдоль Id, а вторые — вдоль самого себя. Эти конструкции позволяют оптимизировать некоторые вычисления и даже построить (ко)монады для произвольного функтора.

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

Расширения Кана представляют собой фундаментальные абстракции, через которые выражается множество других конструкций, применяемых в том числе и в программировании. Но реальная практическая ценность заключается в том, что для расширения Кана разработана специальная техника их вычисления. Этой теме и будет посвящена следующая часть обзора.