Категории типов. Часть 7. Исчисление концов

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

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

Давайте рассмотрим технику исчисления концов через призму теории типов с использованием языка программирования Scala.

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

Hom-типы
Функторы
Естественные преобразования
Монады
Пределы и сопряжения функторов

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

Содержание

Категория запятой
Исчисление концов
Дополнительная литература
Промежуточный итог

Категория запятой

Определение

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

$\begin{split} F:&\; \mathcal{A} \to \mathcal{C}, \\ G:&\; \mathcal{B} \to \mathcal{C}. \end{split}$

Поскольку они приводят в одну категорию $\mathcal{C}$ , то в ней могут существовать морфизмы между объектами образов обоих функторов:

Объект категории запятой — тройка (a,b,f).

Нас интересуют прежде всего такие морфизмы $f,f':\mathrm{Hom}_{\mathcal{C}}$ , которые сохраняют структуру образов функторов и .

В объекты категории запятой входят только такие морфизмы , которые делают такую диаграмму коммутирующей для каких-то . — В объекты категории запятой входят только такие морфизмы $f,\, f'$ , которые делают такую диаграмму коммутирующей для каких-то $h,\, g$ .

Это означает, что должно выполняться соотношение $f' \circ Fh = Gg \circ f$ .

Такие морфизмы $f: \mathrm{Hom}_{\mathcal{C}}(Fa, Gb)$ , вместе с объектами исходных категорий $a:\mathcal{A}$ и $b:\mathcal{B}$ , образуют категорию запятой $F \downarrow G$ с объектами-тройками .

Опять странное название

Эту конструкцию ввели Фрид, Ловер и Маклейн ещё в 1963 году. Первоначально для неё использовали обозначение с обычной запятой в скобках: , которую так и читали «category F comma G». Со временем название «категория запятой» закрепилось как официальный термин, хотя само обозначение изменилось.

Морфизмами категории запятой являются пары морфизмов $(h:\mathrm{Hom}_{\mathcal{A}},\, g:\mathrm{Hom}_{\mathcal{B}})$ , композиция которых $(h, g)\circ(h', g')$ определяется как $(h \circ h', g \circ g')$ .

С категорией запятой связаны два канонических забывающих функтора:

$\begin{split} &\Pi^{\mathcal{A}}: F \downarrow G \to \mathcal{A}, \\ &\Pi^{\mathcal{A}}(a, b, f) = a; \\ \\ &\Pi^{\mathcal{B}}: F \downarrow G \to \mathcal{B}, \\ &\Pi^{\mathcal{B}}(a, b, f) = b; \end{split}$

а также естественное преобразование

$\begin{split} \eta: F \circ \Pi^{\mathcal{A}} \rightsquigarrow G \circ \Pi^{\mathcal{B}}, \\ \eta_{(a, b, f)}:Fa \to Gb = f. \end{split}$

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

Когда мы работаем с эндофункторами в категории типов нам помогает её замкнутость — hom-объекты также являются объектами категории (типами функций). Поэтому в Scala категорию запятой можно закодировать так:

infix type ↓[F[_], G[_]] = [A, B] =>> F[A] => G[B]val commaObject: (List ↓ Option)[String, Int] = // List[String] => Option[Int]  (_: List[String]).headOption.map(_.length)

Может показаться, что здесь получился только последний элемент тройки (String, Int, commaObject). Однако важно понимать, что статически типизированный терм несет в себе и всю информацию о своём типе — имея commaObject мы всегда знаем, что он определён для типов String и Int. Значит, забывающие функторы у нас есть неявно, а каждый экземпляр obj: (List ↓ Option)[A, B] представляет собой компоненту естественного преобразования $\eta_{(A, B, obj)}$ .

Категория (ко)среза

Один из самых простых случаев категории запятой — это срез (slice, слой) категории $\mathcal{C}$ над или под объектом $c:\mathcal{C}$ . Срезы представляют собой категории запятой для тождественного функтора $Id_{\mathcal{C}}$ и константного функтора $\Delta c$ .

Категория среза (над объектом), её объекты и морфизмы определяются следующим образом:

$\begin{split} &\mathcal{C}/c = Id_{\mathcal{C}} \downarrow \Delta c, \\ &(c':\mathcal{C}, f:\mathrm{Hom}_{\mathcal{C}}(c', c)): \mathcal{C}/c, \\ &(h:x \to y\; \text{такой, что}\; g \circ h = f):\mathrm{Hom}_{\mathcal{C}/c}((x,f), (y,g)). \end{split}$

Морфизмы в категории среза устроены так, что они сохраняют значение отображения (второй элемент пары). Например, если мы рассматриваем объект $(Vector[A],\; \_.length)$ в категории $(\star <: Vector[*])/Int$ , то все морфизмы, связанные с этим объектом будут такими функциями h: Vector[A] => Vector[B], которые не поменяют длину вектора! То есть, они фиксируют срез категории всех векторов по заданной длине. Типы векторов в цепочках вычислений внутри категории среза по факту будут зависеть от какого-то значения длины вектора. Категорию среза можно рассматривать как мост между теорией категорий и теорией зависимых типов. Но мы не будем углубляться в эту тему в данном обзоре.

Категория косреза (срез категории под объектом) задаётся дуальным образом:

$\begin{split} &c/\mathcal{C} = \Delta c \downarrow Id_{\mathcal{C}}, \\ &(c':\mathcal{C}, f:\mathrm{Hom}_{\mathcal{C}}(c, c')): c/\mathcal{C}, \\ &(h:x \to y\; \text{такой, что}\; h \circ f = g):\mathrm{Hom}_{c/\mathcal{C}}((x,f), (y,g)). \end{split}$

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

(Ко)конусы и (ко)пределы

Срез категории функторов $\mathcal{D}^{\mathcal{C}}$ над $F: \mathcal{C} \to \mathcal{D}$ даёт категорию конусов , а под ним — коконусы функтора:

$\begin{split} \mathrm{Cone}\, F &= \mathcal{D}^{\mathcal{C}} / F = \Delta \downarrow F, \\ \mathrm{Cocone}\, F &= F / \mathcal{D}^{\mathcal{C}} = F \downarrow \Delta. \end{split}$

Терминальный объект среза $\mathcal{D}^{\mathcal{C}} / F$ — это пара $(\mathrm{Lim}\, F: \mathcal{D},\; \pi: \Delta (\mathrm{Lim}\, F) \rightsquigarrow F)$ , состоящая из предела функтора и естественного преобразования, выражающего универсальное свойство. Дуально, начальный объект косреза $F/\mathcal{D}^{\mathcal{C}}$ даёт копредел функтора $\mathrm{Colim}\, F$ с преобразованием $F \rightsquigarrow \Delta (\mathrm{Colim}\, F)$ .

Сопряжения

Изначально основной задачей категории запятой была формализация сопряжения функторов без упоминания множеств. А именно, функторы $F: \mathcal{C} \to \mathcal{D},\; G:\mathcal{D} \to \mathcal{C}$ сопряжены только тогда, когда изоморфны такие категории запятой (взамен изоморфизма hom-множеств):

$F \dashv\; G \hspace{1cm} \Longleftrightarrow \hspace{1cm} F \downarrow Id_{\mathcal{D}} \cong \; Id_{\mathcal{C}} \downarrow G.$

Если в категории $F \downarrow Id_{\mathcal{D}}$ мы фиксируем $d:\mathcal{D}$ , то получим подкатегорию $F \downarrow d$ , где функтор $d:\mathbb1 \to \mathcal{D}$ просто выбирает этот самый объект . Мы всегда имеем такую категорию запятой для каждого объекта из ко-домена . Её объектами будут пары $(c:\mathcal{C},\;f:Fc \to d)$ . В ней зашифрована как бы «голограмма» категории $\mathcal{C}$ , преобразованной функтором с точки зрения объекта .

Забывающий функтор $\Pi^{\mathcal{C}}_d: F \downarrow d \to \mathcal{C}$ возвращает нас в исходную категорию, сопоставляя каждому $d:\mathcal{D}$ диаграмму в $\mathcal{C}$ . В каждой такой диаграмме будет зашиты те свойства функтора , что выражаются морфизмами в и согласуются со структурой $\mathcal{C}$ .

Так как мы изначально рассматриваем сопряжение $F \dashv G$ , то терминальным объектом категории $F \downarrow d$ будет пара $(Gd,\varepsilon_d)$ , где $\varepsilon_d$ является компонентой коединицы сопряжения. Рассуждая аналогичным образом, получаем начальный объект категории $c \downarrow G$ в виде $(Fc,\eta_c)$ , где $\eta$ — единица сопряжения.

Точечные расширения Кана

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

Рассмотрим два функтора $F:\mathcal{A} \to \mathcal{C}$ и $G:\mathcal{A} \to \mathcal{D}$ . Правое и левое $G \backslash F$ расширения Кана функтора вдоль можно записать как начальный и терминальный объекты в категориях запятой $(\_ \circ G) \downarrow F$ и $F \downarrow (\_ \circ G)$ соответственно, где $\_ \circ G$ — это функтор предкомпозиции функторов. Так как эти полярные объекты сами по себе являются (ко)пределами забывающих функторов, то справедливыми являются следующие формулы:

$\begin{split} &{}_{\_ \circ G}\Pi^{\mathcal{C}^\mathcal{D}} : (\_ \circ G) \downarrow F \to \mathcal{C}^\mathcal{D}, \\ &F / G = \mathrm{Lim}\, {}_{\_ \circ G}\Pi^{\mathcal{C}^\mathcal{D}}; \\ \\ &\Pi^{\mathcal{C}^\mathcal{D}}_{\_ \circ G} : F \downarrow (\_ \circ G) \to \mathcal{C}^\mathcal{D}, \\ &G \backslash F = \mathrm{Colim}\, \Pi^{\mathcal{C}^\mathcal{D}}_{\_ \circ G}. \end{split}$

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

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

А именно, для любого $d:\mathcal{D}$ существует категория запятой $d \downarrow G$ с забывающим функтором ${}_d\Pi^{\mathcal{A}}: d \downarrow G \to \mathcal{A}$ . Этот функтор даёт диаграмму в $\mathcal{A}$ , отражающую «снимок образа с позиции ». Тогда мы можем прокинуть этот снимок в $\mathcal{C}$ с помощью функтора :

$F \circ {}_d\Pi^{\mathcal{A}}: d \downarrow G \to \mathcal{C}.$

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

$\mathrm{Ran}_GF\,d \equiv (F/G)d = \underset{d \downarrow G}{\mathrm{Lim}}\, (F \circ {}_d\Pi^{\mathcal{A}}).$

Аналогично, рассматривая забывающий функтор из категории запятой $\Pi^{\mathcal{A}}_d=G \downarrow d \to \mathcal{A}$ , получаем действие левое расширение Кана в виде копредела:

$\mathrm{Lan}_GF\,d \equiv (G \backslash F)d = \underset{G \downarrow d}{\mathrm{Colim}}\, (F \circ \Pi^{\mathcal{A}}_d).$

Если категория $\mathcal{D}$ (ко)полна (содержит все (ко)пределы), то глобальному определению всегда соответствует точечное определение расширения Кана через (ко)предел. Например, категорию типов языка Scala можно назвать одновременно полной и кополной (с некоторой натяжкой) и расширения Кана функторов, приводящих в неё, имеют поточечное представление.

Записанные таким образом расширения Кана в отдельных точках через (ко)пределы приближают нас к алгоритмам вычислений. Однако эти (ко)пределы берутся по весьма сложно устроенной категории запятой. Даже если получится закодировать их на подходящем языке программирования, реализации всё равно окажутся громоздкими и неудобными для использования. Нам нужно что-то, аналогичное (ко)пределам, но работающее с «простой» категорией $\mathcal A$ .

Исчисление концов

Взвешенные (ко)пределы

Как мы уже видели ранее в обзоре, копредел функтора $K:\mathcal{I} \to \mathcal{C}$ представляет собой сумму объектов категории $\mathcal{C}$ (точнее, образа ), индексированных объектами $i:\mathcal{I}$ . Его универсальное свойство задаётся естественным преобразованием $u: K \rightsquigarrow \Delta\, \mathrm{Colim} F$ , каждая компонента которого является инъекцией (конструктором) этой суммы.

Мы же для левого расширения Кана $G \backslash F$ в точке $d:\mathcal{D}$ получили копредел функтора $H: G \downarrow d \to \mathcal{C} = F \circ \Pi^{\mathcal{A}}_d$ . Копредел берётся по весьма богатой категории запятой, так что элементы получаемой суммы индексированы всеми парами $(a:\mathcal{A}, f: \mathrm{Hom}(Ga, d))$ . Причём, для каждого такого индекса мы имеем $H_{(a,f)}=Fa$ .

Для фиксированного a может существовать огромное (часто бесконечное) «количество» морфизмов . Однако эти морфизмы не задействованы в образе функтора , поэтому каждый даёт вклад в копредел с «весом» $Wa=\mathrm{Hom}(Ga, d)$ . То есть сумма всех $H_{(a,f)}$ по категории запятой превращается во взвешенную сумму $Wa \times Fa$ уже по категории $\mathcal{A}$ .

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

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

$(G \backslash F) d = \underset{G \downarrow d}{\mathrm{Colim}}\, (F \circ \Pi^{\mathcal{A}}_d) = \underset{\mathcal{A}}{\mathrm{Colim}} {}_W \, F.$

Простой копредел обычно не равен полной сумме объектов образа функтора. Это возможно лишь когда функтор определён на дискретной категории, а в противном случае универсальное свойство «фильтрует» члены суммы в соответствии со структурой морфизмов исходной категории. У взвешенных копределов условия ещё более жёсткие — их нельзя свести к простому копределу от $W\, a \times Fa$ . Дело в том, что вес оказывается контравариантным функтором, что делает всё произведение инвариантным. Чтобы можно было вычислить взвешенный копредел, универсальное свойство копредела по категории запятой накладывает дополнительные ограничения на члены суммы.

И прежде чем будем разбираться с этими ограничениями, рассмотрим сперва дуальную картину. Для правого расширения Кана в точке $d:\mathcal{D}$ мы получили предел функтора $H: d \downarrow G \to \mathcal{C} = F \circ {}_d\Pi^{\mathcal{A}}$ . Все объекты дают вклад в предел «ровно раз». Учёт веса $Wa=\mathrm{Hom}(d, Ga)$ приводит нас к произведению по индексу $a:\mathcal{A}$ от экспоненциалов $\mathrm{Hom}(\mathrm{Hom}(d, Ga), Fa)$ . Обратите внимание — эта конструкция также получается инвариантной по индексу , что опять же не позволяет вычислить её обычный предел. Зато взамен мы получаем взвешенный предел:

$(F / G) d = \underset{d \downarrow G}{\mathrm{Lim}}\, (F \circ {}_d\Pi^{\mathcal{A}}) = \underset{\mathcal{A}}{\mathrm{Lim}} {}_W \, F.$

Диестественные преобразования

Коконус копредела $X = \mathrm{Colim}\,F$ функтора $F:\mathcal{C} \to \mathcal{D}$ задаётся естественным преобразованием $\alpha: F \rightsquigarrow \Delta X$ . На компоненты преобразования накладываются условие естественности: для любого морфизма $f:\mathrm{Hom}_{\mathcal{C}}(a,b)$ должно выполняться равенство $\alpha_a = \alpha_b \circ Ff$ (так как $\Delta Xf = id$ ).

В категории запятой морфизмы $\mathrm{Hom}_{\mathcal{G \downarrow d}}((a,f),(a',f'))$ представляют такие функции $h:a\to a'$ , что $f=f'\circ G h$ . Забывающий функтор ${}_d\Pi^{\mathcal{A}}$ , действуя на эти морфизмы, возвращает просто . Учитывая всё это, запишем условие естественности для универсального свойства копредела так:

$\alpha_{(a,f'\circ G h)} = \alpha_{(a',f')} \circ Fh.$

Компоненты естественного преобразования являются функциями над объектами в $\mathcal{D}$ , но они также параметризованы и . Нам же нужно получить другое преобразование с компонентами $\phi_a:\mathrm{Hom}(Ga,d) \to \mathrm{Hom}(Fa,X) \equiv \alpha_{(a,f)}$ . Учитывая, что весовой функтор действует на морфизмы как $Whf' = f' \circ Gh$ , перепишем наше требование в виде

$(\phi_a \circ Wh)f' = \phi_{a'}(f') \circ Fh. \hspace{2cm}(LimDinat)$

По сути, $\phi_a$ — это функция, возвращающая функцию, и мы можем выполнить её декаррирование: $\phi_a(f:\mathrm{Hom}(Ga,d))(fa:Fa):X \equiv \hat\alpha_a(f, fa)$ . Так что, используя введённый ранее весовой функтор $Wa=\mathrm{Hom}(Ga, d)$ , можем записать

$\hat\alpha_a: Wa \times Fa \to X.$

Конструкция $P(a,a'): \mathcal{A}^{op} \times \mathcal{A} \to \mathcal{V} = Wa \times Fa’$ , очевидно, является профункторм. С правой же стороны у нас стоит копредел , который можно записать через константный профунктор (с тривиальным действием на морфизмы). В итоге получаем, что $\hat\alpha$ — это преобразование профункторов на диагонали:

$\begin{split} \hat\alpha_a&: P(a,a) \to Q(a,a),\\ \hat\alpha&: P \ddot{\rightsquigarrow} Q. \end{split}$

Оно называется диестественным преобразованием профункторов и . Условие диестественности определяется коммутированием следующей диаграммы:

Условие диестественности преобразования . — Условие диестественности преобразования $\hat\alpha$ .

Алгебраически оно записывается так:

$Q(id_a,h) \circ \alpha_a \circ P(h,id_a) = Q(h,id_{a'}) \circ \alpha_{a'} \circ P(id_{a'},h).$

Если подставить сюда константный профунктор вместо , то равенство упростится до .

Аналогично, рассматривая предел в категории запятой для правое расширения Кана мы приходим диестественному преобразованию из константного бифунктора в профунктор $P(a,a')=\mathrm{Hom}(\mathrm{Hom}(d,Ga),Fa')$ .

Тогда как обычные (ко)пределы являются универсальными (ко)конусами, задаваемые естественными преобразованиями, взвешенные (ко)пределы — это универсальные клинья (wedges) и коклинья (cowedges) — диестественными преобразованиями.

Ещё один странный термин.

Если «конусы» достаточно легко находятся на диаграммах, то с «клиньями» дело немного сложнее. Дело в том, что у профунктора есть два аргумента, значит есть два разных пути его модификации одним морфизмом . На диаграмме это выглядит как две стрелки, связанные в «вершине». Математики увидели на таких диаграммах именно «клинья» (или коровьи рога?))).

Стоит отметить, что диестественное преобразование профункторов $\hat\alpha: P \,\ddot\rightsquigarrow\, Q$ слабее естественного $\alpha: P \rightsquigarrow Q$ , определённого в категории пар $\mathcal{A}^{op} \times \mathcal{A}$ . Последнее требует коммутативности более сложной диаграммы, получаемой из представленной выше путём добавления в центре дополнительного узла и трёх связанных с ним стрелок:

«Естественность» применяется к каждому аргументу профунктора независимо друг от друга. Это условие оказывается значительно более строгим, чем диественность, значит оно оставляет меньше членов в сумме/произведении и оказывается гораздо беднее.

В программировании обеспечить диестественность помогают бесплатные теоремы параметрического полиморфизма. Вот пример типа преобразования на Scala, и как его можно использовать:

infix type ⇻[P[-_, +_], Q[-_, +_]] = [A] => P[A, A] => Q[A, A]    type Codec[-A, +B] = ( // нетривиальный профунктор  encode: A => String,    decode: String => Option[B]  )  type FuncOpt = Kleisli[Option] // A => Option[B]  val codecChecker: Codec ⇻ FuncOpt =    [A] => (codec: Codec[A, A]) => codec.decode `compose` codec.encode  val codec: Codec[Int, Int] = (_.toString, _.toIntOption)  codecChecker(codec)(42) // Some(42)

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

Области значений профункторов

Теория категорий изначально строилась на фундаменте теории множеств, и там часто используются соответствующие конструкции, вроде $f \in \mathrm{Hom}(a, b)$ . Вообще, в приложении к программированию стараются использовать только малые категории, то есть те, морфизмы в которых образуют множества $\mathrm{Hom}(a, b): \mathcal{Set}$ .

В данном же обзоре я по возможности избегал упоминания множеств и связанных с ними конструкций, предпочитая язык теории типов ( $f: \mathrm{Hom}(a, b)$ ). Дело в том, что типы не являются множествами значений, и я регулярно стараюсь развеять этот миф. Теория типов (лямбда-исчисление) — конструктивная наука, полезная в реальном мире, в частности, в программировании. Тогда как практическая полезность неконструктивной теории множеств оказывается существенно ограниченной.

Особую актуальность эти нюансы приобретают именно сейчас, когда мы вовсю начинаем вертеть профункторами. У того же Милевски рассматриваются профункторы вида $P: \mathcal{C}^{op} \times \mathcal{C} \to \mathcal{Set}$ и при переходе к программированию они трансформируются в $P: \mathcal{Type}^{op} \times \mathcal{Type} \to \mathcal{Type}$ . То есть Милевски изначально не делает больших различий между типами и множествами. Я же пошёл на небольшую хитрость — стараюсь вообще не упоминать, в какую категорию действует профункторы, ведь это действительно не принципиально! Зато в конце мы сразу оказываемся в единственной категории $\mathcal{Type}\equiv\star$ . Свести концы с концами нам помогает её замкнутость — суммы, произведения и экспоненциалы объектов принадлежат той же категории.

(Ко)концы профункторов

Для нас прежде всего важны клинья и коклинья — диестественные преобразования, связанные с константным профунктором. Такие преобразования представляют произвольный профунктор в виде отдельных объектов. (Ко)клинья определяются через константный профунктор:

type ΔΔ[X] = [A, B] =>> X  // констатный профунктор/бифункторtype   Wedge[P[-_, +_]] = [A] =>> ΔΔ[A] ⇻ P  //   Клин [A] => X => P[A,A]type Cowedge[P[-_, +_]] = [A] =>> P ⇻ ΔΔ[A]  // Коклин [A] => P[A,A] => X

И конечно же, наиболее интересны самые универсальные из них — терминальный и начальный объекты в категориях клиньев и коклиньев соответственно.

Универсальный клин называется концом профунктора. По сути, он является терминальным объектом в категории клиньев. Хоть и математически следующая цепочка равенств не достаточно точна, но она демонстрирует конструктивный вывод конца профунктора как клина для терминального объекта :

$\begin{split} \mathrm{End}\,P& \\ &=\underset{x}{\mathrm{Lim}} (\Delta x \,\ddot\rightsquigarrow\, P) &&\text{терминальный объект в категории клиньев} \\ &\cong(\underset{x}{\mathrm{Colim}}\, \Delta x) \,\ddot\rightsquigarrow\, P &&\text{контравариантость превращает в копредел} \\ &\cong\Delta (\underset{x}{\mathrm{Colim}}\, Id_x) \,\ddot\rightsquigarrow\, P \hspace{1cm}&&\text{особенности константного функтора} \\ &=\Delta 1 \,\ddot\rightsquigarrow\, P. &&\text{универсальное свойство терминального объекта} \end{split}$

Здесь учтено, что

при пробрасывании предела в левую часть $\ddot\rightsquigarrow$ из-за контравариантности обращаются все стрелки и мы получаем копредел;
копредел константного профунтора преврщается в константу от копредела тождественного функтора,
который суть терминальный объект категории (их универсальные свойства совпадают).

Значит на Scala конец профунктора можно записать так:

type End[P[-_, +_]] = Wedge[P][Unit] // ΔΔ[Unit] ⇻ P = [A] => Unit => P[A, A]

По сути, это универсальное произведение диагональных элементов профунктора. Условие диестественности учитывает только универсальные закономерности для профунктора, не влияющие на выбор проекции. Конкретные объекты a могут иметь и свои отличительные особенности, «but in the end, it doesn’t even matter»©.

С другого конца дело выглядит несколько сложнее. Коконец является начальным (копредельным) объектом в категории коклиньев, так что в результате получается универсальная сумма диагональных элементов. Её можно реализовать как экзистенциальный тип:

trait Coend[P[-_, +_]]:    type A    val p: P[A, A]

Конструкторы реализаций этого трейта будут соответствовать компонентам диестественного преобразования — универсального свойства коконца.

Экзистенциальные типы, как и любые другие, полезны способами использования (их значений). Здесь нам неизвестен тип A, поэтому чтобы что-то сделать с хранимым p: P[A, A] обязательно потребуется полиморфная функция типа [X] => P[X, X] => R. Похоже на определение клина, не правда ли? Категориально эту ситуацию мы можем описать так:

$\begin{split} \mathrm{Coend}\,P &= \underset{x}{\mathrm{Colim}} (P \,\ddot\rightsquigarrow\, \Delta x) = \mathrm{End}\, Q, \\ Q(a,b) &= (P \,\ddot\rightsquigarrow\, \Delta a) \to b. \end{split}$

В коде это выглядит следующим образом:

type CoendProf[P[-_, +_]] = [A, B] =>> Cowedge[P][A] => B // преобразование профунктораtype Coend[P[-_, +_]] = End[CoendProf[P]] // [R] => Unit => Cowedge[P][R] => R

Конкретно здесь полезно избавиться от Unit, записав

type Coend[P[-_, +_]] = [R] => Cowedge[P][R] => R // [R] => ([A] => P[A, A] => R) => R

Коконец профунктора в теории категорий обозначается так (обратите внимание на верхнее положение индекса):

$\int^c P(c,c).$

Это сумма диагональных элементов профунктора, «склеенных» (факторизованных) условием диестественности. Использование знака интеграла обусловлено тем, что суммирование производится по единому связному пространству категории, «непрерывной» в том смысле, что её объекты связаны морфизмами. В определении (ко)конца за учёт этих связей отвечает как раз условие диестественности.

Универсальное свойство коконца профунктора.

Компоненты диестественного преобразования $i:P \,\ddot\rightsquigarrow\, \Delta_{\mathrm{Coend}\,P}$ представляют собой конструкторы (инъекторы) коконца $i_a: P(a,a) \to \mathrm{Coend}\,P$ . Универсальное свойство определяется так: для любого кандидата x с отображением $\alpha_a:P(a,a) \to x$ существует единственный морфизм $u:\mathrm{Coend} \to x$ , такой что $\alpha_a = u \circ i_a$ .

Аналогично, универсальный клин носит название конец (end) профунктора:

$\mathrm{End}\,P = \Delta1 \,\ddot\rightsquigarrow\, P = \int_c P(c,c).$

Универсальное свойство конца профунктора.

Индекс интеграла конца пишется снизу, и теперь это произведение диагональных элементов профунктора, «профильтрованных» условием диестественности. Компоненты преобразования $\pi: \Delta(\mathrm{End}\,P) \,\ddot\rightsquigarrow\, P$ представляют собой проекторы конца $\pi_a: \mathrm{End}\,P \to P(a,a)$ . Универсальное свойство определяется так: для любого кандидата x с отображением $\alpha_a: x \to P(a,a)$ существует единственный морфизм $u: x \to \mathrm{End}$ , такой что $\alpha_a = \pi_a \circ u$ .

(Ко)конец как (ко)уравнитель

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

Условие диестественности, отбрасывающее члены (ко)произведения, заключается в коммутативности диаграммы — в эквивалентности двух путей. То есть, выживают только те члены, для которых эти пути равны. В такой форме, эти условия соответствуют универсальным свойствам (ко)уравнителя — (ко)предела хитрого функтора в специальной «категории разбиения» (subdivision category) $\mathcal{A}^\$$ . Данный термин использовал Саундерс Маклейн в своей книге «Категории для работающего математика». Таким образом, (ко)концы являются полноценными (ко)пределами и обладают соответствующими свойствами, вроде (ко)непрерывности и перестановочности с другими (ко)пределами.

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

$\begin{split} \int^c G \times F(c, c) &\cong G \times \int^c F(c, c), &&\hspace{1cm}\text{дистрибутивность} \\ \int_a\int_b F(a,b;a,b) &\cong \int_b\int_a F(a,b;a,b), &&\hspace{1cm}\text{теорема Фубини для (ко)концов} \\ \mathrm{Hom}\left( \int^c F(c,c),\, G \right) &\cong \int_c \mathrm{Hom}\left(F(c,c),\, G \right). &&\hspace{1cm}\text{каррирование} \end{split}$

Последнее соотношение использовалось выше для превращения коконца в конец посредством кодирования Чёрча. Ещё несколько примеров мы посмотрим далее.

Естественные преобразования

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

Наиболее обобщённая «стрелка» между функторами и — это профунктор $P(a,b)=\mathrm{Hom}(Fa,Gb)$ . И всё самое ценное содержится на диагонали этого профунктора. То есть, буквально, отношения между функторами описываются сразу всеми компонентами диагонали. Таким образом, морфизм между двумя функторами определяется через конец:

$\int_c \mathrm{Hom}(Fc,Gc): F \rightsquigarrow G.$

В Scala это реализуется так:

infix type ~>[F[+_], G[+_]] = End[F ↓ G] // [A] => Unit => F[A] => G[A]

Строго говоря, категория запятой $F \downarrow G$ не является профунктором. Эти понятия тесно связаны — категория запятой является категорией элементов профунктора, но это выходит за рамками данного обзора. Поэтому определённая ранее конструкция F ↓ G как нельзя лучше подходит, чтобы запрограммировать преобразования через конец.

Стрелка из Unit в этом типе «лишняя», и при вычислении конца таким способом придётся постоянно приписывать (()). Это следствие ограничений Scala на типы полиморфных функций. Впрочем, всегда можно определить свой класс с теми же возможностями, но без «неудобных приписок».

Композиции профункторов

Во второй части обзора при обсуждении профункторов была опущена очень важная особенность — их можно рассматривать как морфизмы между категориями. В частности, профункторы вида $\mathcal{A}^{op} \times \mathcal{B} \to \mathcal{V}$ считаются стрелками $\mathcal{A} \nrightarrow \mathcal{B}$ (в некоторых источниках по определённым причинам пишут наоборот $\mathcal{B} \nrightarrow \mathcal{A}$ , но здесь мы будем придерживаться более очевидной нотации).

Комбинировать профункторы можно посредством коконцов. А именно, композиция $P \circ Q: \mathcal{A} \nrightarrow \mathcal{C}$ профункторов $P:\mathcal{A} \nrightarrow \mathcal{B}$ и $Q:\mathcal{B} \nrightarrow \mathcal{C}$ стоится так:

$(Q \circ P)(a,c) = \int^b P(a,b) \times Q(b,c).$

Тут идея вот в чём: комбинируя профункторы мы стыкуем шаги вычислений, содержащиеся в их компонентах. Значит нам буквально нужны произведения $P(a,b) \times Q(b',c)$ . Чтобы удовлетворять условиям функториальности, эти шаги обязаны стыковаться «на диагонали» . Так как мы ищем совокупность всех путей для разных b, то это будет именно «сумма» по , а не произведение. Наконец, требование диестественности склеит вклады эквивалентных путей.

Эта формула неспроста напоминает матричное умножение $(QP)_{ac}=\sum_b P_{ab} \cdot Q_{bc}$ . Ведь матрицы также являются стрелками-операторами между векторными пространствами, как и профункторы соединяют отдельные категории.

Вот как композиция профункторов реализуется в Scala (оператор × уже не раз использовался в обзоре как синоним кортежа):

type TProd[P[-_, +_], Q[-_, +_]] = [A, D] =>> [B, C] =>> P[A, C] × Q[B, D]  infix type ProfCompose[Q[-_, +_], P[-_, +_]] = [A, C] =>> Coend[TProd[P, Q][A, C]]// [A, C] =>> ([R] => ([B] => (P[A,B] × Q[B,C]) => R) => R)

Хитровато выглядит, не так ли?) Посмотрим, как комбинируются два простых профунктора:

type P  = Id ↓ Option   // A => Option[B]  type Q  = Option ↓ List // Option[A] => List[B]  type QP = Q ProfCompose Psummon[QP[Int, String] =:= ([R] => ([A] => ((Int => Option[A], Option[A] => List[String])) => R) => R)]

Можно было ожидать, что в итоге получится тип, изоморфный QPExp[A, B] = A => List[B]. И действительно, всегда существует такое естественное преобразование профункторов:

type QPExp = Id ↓ List // ожидаемый профункторval nat: [A, B] => QP[A, B] => QPExp[A, B] = // естественное преобразование  [A, B] => qp => a =>      qp([X] => (pair: P[A, X] × Q[X, B]) => pair._2(pair._1(a)))

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

На базе профункторов можно построить новую категорию категорий, отличную от всех, что упоминались в обзоре ранее. Композицию таких морфизмов мы уже обсудили, а в качестве тождественных выступают профункторы $ID_\mathcal{A}\colon \mathcal{A} \nrightarrow \mathcal{A} = \mathrm{Hom}_{\mathcal{A}}$ .

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

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

Взвешенные (ко)пределы и расширение Кана

Ранее мы видели, что взвешенные (ко)пределы функтора по весу — это суммы и произведения, члены которых «склеены» или «профильтрованы» условием диестественности. Иными словами, это буквально (ко)концы профункторов, собранных из и . Например, взвешенный копредел вычисляется так:

$\mathrm{Colim}_WF = \int^{d:\mathcal{D}} W(d) \times F(d).$

Суммирование производится по диагонали профунктора $P(d,d')=W(d) \times F(d')$ . Напомню, для копредела вес должен быть контравариантен.

В свою очередь, взвешенный предел будет концом профунктора $Q(d,d') = \mathrm{Hom}(W'(d), F(d'))$ :

$\mathrm{Lim}_WF = \int_{d:\mathcal{D}} \mathrm{Hom}(W'(d), F(d)).$

Применяя эти формулы для расширений Кана функтора вдоль в точках, получаем:

$\begin{split} &G\backslash F\, a = \int^d \mathrm{Hom}(Gd,a) \times Fd, \\ &F/G\, a = \int_d \mathrm{Hom}\big(\mathrm{Hom}(a,Gd),\, Fd\big). \end{split}$

И теперь мы можем реализовать эти формулы в коде.

type   WLimit[W[+_]] = [F[+_]] =>>   End[[A, B] =>> W[A] => F[B]]  type WColimit[W[-_]] = [F[+_]] =>> Coend[[A, B] =>> W[A]  × F[B]]type ProdWeight[G[+_], A] = [D] =>> A => G[D]  // вес для Rantype  SumWeight[G[+_], A] = [D] =>> G[D] => A  // вес для Laninfix type /[F[+_], G[+_]] = [A] =>>   WLimit[ProdWeight[G, A]][F]  infix type \[G[+_], F[+_]] = [A] =>> WColimit[ SumWeight[G, A]][F]summon[(F / G)[A] =:= ([R] => Unit => (A => G[R]) => F[R])]  summon[(G \ F)[A] =:= ([R] => ([X] => (G[X] => A) × F[X] => R) => R)]

В правом расширении Кана можно избавиться от стрелки из Unit и явно записать такой изоморфный тип:

type Ran[F[_], G[_]] =  // ≅ (F / G)[A]  [A] =>> [R] => (A => G[R]) => F[R]

Именно в таком виде (или по ООП-шному через отдельный класс) эта конструкция встречается в библиотеках.

Левое же расширение Кана «усложнено» кодированием Чёрча для экзистенциального типа-суммы. Поэтому часто его реализуют посредством изоморфного обобщённого алгебраического типа (GADT):

enum Lan[F[_], G[_], A]:  // ≅ (G \ F)[A]  case Cell[F[_], G[_], A, B](f: F[B] => A, g: G[B]) extends Lan[F, G, A]

Конструкторы Lan.Cell[F, G, A, B] являются компонентами диестественного преобразования — универсального свойства расширения Кана. Они параметризированы дополнительным типом B, который «прячется» внутри каждого значения Lan[F, G, A] и мы знаем лишь, что «он существует» (экзистенциальность). Извлечь его помогает механизм сопоставления с шаблонами. Не сказал бы, что такая реализация левого расширения Кана действительно проще изначальной, но она привычнее для большинства программистов.

Сильные расширения Кана

В большинстве современных языков программирования мы имеем дело с декартово замкнутой категорией типов. (Би)декартовость подразумевает, что для всех типов есть также реализации их произведений (кортежи, классы…) и сумм (обычно, через ООП-шное наследование). То есть, в категории есть пределы и копределы всех диаграмм. Замкнутость категории означает обогащённость над собой — экспоненциалы любых типов также являются типами (типы функций, как правило, реализуемые через метод класса). Hom-изоморфизмы будут изоморфизмами обычных объектов-типов.

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

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

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

Universal Properties II: Comma Categories пост в личном блоге Брайана Хеплера
Из блога Кафе программирования Бартоша Милевски:
- Ends and Coends
- Natural Transformations and Ends
- Pointwise Kan Extensions (тут и про категорию запятой есть параграф)
Ends пост Саймона Уиллертона в блоге The n-Category Café
Kan Extensions III: As Ends and Coends пост Эдварда Кметта в блоге The Comonad.Reader
Coend calculus толстая теория от Фоско Лореджана в формате pdf
Реализация KanExtensions.scala из библиотеки Meow Цзичао Оуяна

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

Исчисление теории категорий завязано на «морфизмах между морфизмами», что в программировании соответствует (полиморфным) функциям высокого рода.
Одной из базовых абстракций, описывающей отношение между функторами, является категория запятой. Её объекты представляют собой совокупности морфизмов между образами этих функторов.
Категории запятой предоставляют унифицированный способ описания сопряжений и (ко)конусов функторов. Кроме того, расширения Кана можно представить как (ко)пределы в категориях запятых.
Но вычислять (ко)пределы в этих категориях сложно. Поэтому от них переходят к взвешенным (ко)пределам в исходных категориях. В них вклад функтора в каждой точке идёт с определённым «весом».
Учёт таких весов оказывается контравариантным по отношению к исходному функтору, так что взвешенные (ко)пределы представляют собой своеобразные суммы и произведения от значений профункторов, собранных из функтора и веса в точках.
Универсальные свойства взвешенных (ко)пределов теперь описываются диестественными преобразованиями полученных профункторов.
Фильтрация (или «склеивание») членов сумм и произведений посредством условия диестественности обобщается на произвольные профункторы. В итоге приходим к понятиям (ко)концов профункторов.
В программировании диестественная фильтрация произведений в точности соответствует параметрическому полиморфизму, поэтому концы реализуются просто как полиморфные функции.
Коконцы можно записать в Scala как минимум тремя разными способами: с помощью кодирования Чёрча, типа-перечисления (GADT) или типа, зависящего от пути (path-dependent types).
Исчисление концов показывает, в частности, как комбинировать профункторы, вычислять естественные преобразования и расширения Кана.

Осталось только разобраться, как это всё богатство помогает конструировать монады)).

ссылка на оригинал статьи https://habr.com/ru/articles/1023452/