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

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

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

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

8.1. Вертикальная композиция эффектов

8.2. Горизонтальная композиция эффектов

Итоги

Содержание

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

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

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

Пусть у нас есть функтор и нам нужно найти для него такой , чтобы существовало сопряжение $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}$ , различить их только на основе морфизмов из образа.

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

UPD. Убрано бесполезное упоминание конструкции F/(F/Id).

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

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

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

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

$\mathrm{Free}\, F = U / 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$ (гомоморфизмы алгебр функтора). Действие забывающего функтора на морфизмы тривиально, а из объектов он просто выбрасывает второй элемент пары. Поэтому можно считать, что для любого автоматически задан такой забывающий функтор.

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

Здесь мы не получаем изоморфизма с исходным функтором: $\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_{\mathcal{Kl}} \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} / \tilde{U},$

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

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

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

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

Идея оптимизации вычисления цепочек flatMap с помощью техники продолжений для свободной монады стала популярной благодаря работам Олега Киселёва:

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

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

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

В продолжении обзора мы рассмотрим устройство свободной монады подробнее.

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

Пусть у нас есть монада $(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, а вторые — вдоль самого себя. Эти конструкции позволяют оптимизировать некоторые вычисления и даже построить (ко)монады для произвольного функтора.

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

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

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