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

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

Универсальные свойства типов

В одной из предыдущих частей обзора был продемонстрирован функтор, связывающий две разные категории одного и того же объекта — категории типов . Только в начальной категории морфизмами выступали конструкторы типов F[_], а в конечной — эндофункторы Functor[F]. Полученный функтор сохранял композицию конструкторов типов, позволяя из любых Functor[F] и Functor[G] создавать Functor[G ∘ F]. А это, в свою очередь, означает, что если имеются реализации эндофункторов для каких-либо базовых F[_], у нас автоматически есть эндофункторы для абсолютно любых контейнерных типов!

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

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

В качестве примера напомню универсальное свойство произведения объектов:

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

Определение любого универсального свойства в категории имеет такую структуру:

• обозначаются объекты, через которые формулируется универсальный (для произведения и суммы — это просто пара объектов );

• выбирается семейство кандидатов с определёнными возможностями (в примере выше — пары морфизмов или );

• для каждого кандидата определяется морфизм , связывающий его с целевым универсальным объектом;

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

Как перечисленные пункты описать в терминах категории типов? «Возможности» кандидата — это некие преобразования, связывающие его с объектами подкатегории, фиксирующими формулировку универсального свойства. А требование коммутируеммости диаграммы очень напоминает условие естественности этого преобразования!

Конечно же, тут подразумевается некая функториальность для конструктора типов F[_, ...]. Его параметры даже могут иметь разную вариантность, поэтому в общем случае придётся иметь дело с мультипрофункторами, но в этой статье мы будем иметь дело, в первую очередь, с ковариантными функторами и бифункторами.

Конусы и ко-конусы

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

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

Ещё нам нужно выбрать объект-кандидат . Поручим это константному функтору . Естественное преобразование называется конусом функтора :

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

Образ функтора образует подкатегорию , являющуюся «основанием» этого конуса, а объект будет его вершиной:

Для универсального свойства суммы объектов получим дуальную картину. Напомню,

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

На диаграмме получаем как бы «перевёрнутый конус»:

Обратите внимание, что и моделирующая категория и функтор остались теми же, что и для произведения типов! Изменилось только направление естественного преобразования.

Кандидаты в универсальные объекты можно выразить либо через конусы, либо ко-конусы. Осталось только выбрать среди них тот самый универсальный (если он вообще существует).

Пределы и копределы

Чуть позднее мы рассмотрим этот аспект подробнее, а сейчас вернёмся к формализации (ко)пределов.

Итак, предельное универсальное свойство утверждает, что «…для каждого кандидата существует единственный морфизм в предел...». Очевидно, что речь идёт о взаимно-однозначном соответствии кандидатов и морфизмов между ними и пределом. Кандидаты представлены своими конусами, которые можно рассматривать как контравариантный функтор

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

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

Часто (в том числе у Милевски) предполагается, что категории и являются малыми, так что морфизмы между их объектами образуют множества. Тогда оба hom-функтора не только исходят из одной и той же категории, но и приводят в одинаковую категорию множеств: . В этом случае, требуемую «взаимную однозначность» можно выразить через естественный изоморфизм этих функторов (каждому кандидату по универсальному морфизму!):

В компонентах получается такая диаграмма:

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

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

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

(Ко)пределы в категории типов

Как вообще можно построить новые типы? Исходно у нас нет возможности сделать что-то интересное с одним единственным типом, кроме как вернуть его же. Но можно попробовать скомбинировать пару существующих типов в какой-то новый. Получится функциональное отображение, на вход которому подаётся два типа, а на выходе получаем один новый. Это просто «двухдырочные» конструкторы типов вида (*, ) => . Их можно трактовать как функторы из произведения категорий типов в неё же: . Произведение двух категорий типов моделируется дискретной категорией , состоящей из двух индексов и , так что наши бифункторы можно записать как . Конусами этих бифункторов будут естественные преобразования c компонентами, индексированными двумя объектами :

type Cone2[A, B] = [-C] =>> ( // C - кандидат
  C => A, // первая компонента естественного преобразования
  C => B  // вторая компонента естественного преобразования
)

С другой стороны у нас hom-тип, описывающий морфизмы из кандидата в предел:

type ULim[A, B] = [-C] =>> C => Lim[A, B]

Нам нужно выяснить, каким же может быть Lim[A, B], чтобы эти контравариантные функторы для Cone2[A, B][-_] и ULim[A, B][-_] образовывали естественный изоморфизм

infix type ≅[F[_], G[_]] = (
  right: F ~> G,
  left : G ~> F,
)

summon[Cone2[A, B] ≅ ULim[A, B]]

К счастью, мы заранее знаем, что пределом будет произведение типов. В этом мы убедимся, реализовав изоморфизм:

type Lim[A, B] = A × B // (A, B)

given limIso: [A, B] => Cone2[A, B] ≅ ULim[A, B] = (
  right = [C] => (cone: (C => A, C => B)) => (c: C) => cone._1(c) -> cone._2(c),
  left  = [C] => (ulim: C => A × B) => (ulim andThen {_._1}) -> (ulim andThen {_._2})
)

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

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

Формально, можно вывести несколько разных вариантов одного и того же предела функтора. Например, произведение типов можно описать с помощью кодирования Чёрча как [A, B] =>> [C] => (A => B => C) => C. Но для всех этих вариантов в левой части естественный изоморфизма будут всё те же конусы, а значит и правые части будут изоморфны для всех вариантов. Таким образом, предел функтора единственен с точностью до изоморфизма (если он вообще существует).

Аналогично, убеждаемся, что копределом бифунктора будет сумма типов:

type Cocone2[A, B] = [+C] =>> ( // C - кандидат
  A => C, // первая компонента естественного преобразования
  B => C  // вторая компонента естественного преобразования
)
type UColim[A, B] = [+C] =>> Colim[A, B] => C

type Colim[A, B] = A + B // A Either B

given colimIso: [A, B] => Cocone2[A, B] ≅ UColim[A, B] = (
  right = [C] => (cocone: (A => C, B => C)) => (colim: Colim[A, B]) =>
    colim.fold(cocone._1, cocone._2),
  left  = [C] => (ucolim: (A + B) => C) =>
    ((a: A) => ucolim(Left(a)), (b: B) => ucolim(Right(b)))

В случае бо́льших размеров категории наиболее близкой реализация копредела в Scala будет, пожалуй, перечисление подобного вида:

enum Sum3[A, B, C]: // три конструктора:
  case One(a: A)
  case Two(b: B)
  case Tri(c: C)

Для экспоненциала в категории типов (то есть, функций A => B) также существует конструкция, которую можно интерпретировать как предел константного функтора . Но теперь категория индексов будет дискретной категории значений типа A. Компоненты конусов кандидатов будут иметь вид:

// типы A и B фиксированы
// компонетны конуса индексированы значениям A
type ConeDelta = [-C] =>> A => (C => B)
type ULimExp   = [-C] =>> C => LimExp

type LimExp = A => B

given expIso: ConeDelta ≅ ULimExp = (
  right = [C] => (cone: A => C => B) =>
    (c: C) => (a: A) => cone(a)(c)
  left  = [C] => (ulim: C => A => B) =>
    (a: A) => (c: C) => ulim(c)(a)
)

Изоморфизм функторов отражает простое алгебраическое соотношение , его морфизмы суть просто частичное применение каррированных функций.

Итак, мы можем строить новые типы складывая, умножая и «возводя в степень» существующие. А как определяются универсальные свойства нулевого и единичного типов, «существующих изначально»? Да совершенно аналогичным способом! Только если раньше мы строили новые типы из двух, моделируемых категорией , теперь нам не требуется ни одного типа, что соответствует абсолютно пустой категории . Единственно возможный функтор честно отображает пустую категорию в пустую диаграмму в , и от (ко)конусов остаются одни лишь вершины-кандидаты. В случае предела полученного функтора все универсальные морфизмы будут вести к нему, в то время как для копредела они будут вести от него к кандидатам. Это в точности соответствует универсальным свойствам терминального и начального объектов в категории типов — единичного (Unit) и нулевого (Nothing) типов!

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

• предел и копредел диаграммы (помимо тождественных, есть два дополнительных морфизма между объектами) — уравнитель и коуравнитель функций морфизмов;

• предел диаграммы — декартов квадрат (расслоённое произведение, pullback);

• копредел диаграммы — кодекартов квадрат (расслоённая сумма, амальгама, pushout).

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

Непрерывность и когерентность функторов

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

(Напомню, предел — это функтор, определённый на категории функторов. То есть, его можно как композировать с другими функторами, так и применять к ним.)

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

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

Среди эндофункторов в категории типов непрерывно-когерентным будет только тождественный функтор.

Сопряжения функторов

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

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

В целях обобщения, попробуем реорганизовать эти конструкции, избавившись от упоминания и . Сперва для наглядности перепишем их через hom-объекты:

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

Аналогично, если в правую ветку вместо подставить , и передать туда , получим

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

Преобразования называется «единицей» сопряжения. Его можно визуализировать так:

Дуально, преобразование называются «коединицей»:

Между ними существуют очевидные условия консистентности — приведённые ниже треугольники должны коммутировать:

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

Зато его можно интерпретировать как «ослабленную эквивалентность категорий» для случаев, когда строгая эквивалентность не нужна. Действительно, категории и считались бы эквивалентными, если бы для встречных функторов и между ними существовали бы натуральные изоморфизмы: и . А в случае сопряжений не нужны полные изоморфизмы, состоящие из четырёх естественных преобразований — достаточно лишь двух из них: и .

Монады и комонады

В примере с диагональным функтором и пределом приходилось работать не только с привычной категорией типов , но и с «неудобной» категорией функторов . И также получается со многими сопряжениями — даже если какая-та категория нам и интересна, то с другой может и не повезти. Тогда какая может быть практическая польза от этих сопряжений?

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

Действительно, «запаковка» и «распаковка» совпадают с единицей и коединицей сопряжения, а «разматрёшивание» и «заматрёшивание» выражаются так:

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

Тут очень хорошо просматривается дуализм монады и комонады. Если первая строится для композиции сопряжения , то вторая получается автоматически, но уже для перестановки . В предыдущей части обзора мы уже видели похожую картину. Тогда для эндофункторов, соответствующих Writer[L] = [X] =>> L × X и Reader[R] = [X] =>> R => X, одна их композция давала монаду State[S] = Reader[S] ∘ Writer[S], а другая — комонаду Store[S] = Writer[S] ∘ Reader[S]. Можно ожидать, что Writerи Reader образуют сопряжение, и так оно и есть — мы убедимся в этом далее.

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

Сопряжённая тройка

Ранее мы видели, что для каждого функтора существует лишь единственный предел (для простоты не будем больше добавлять «с точностью до изоморфизма»). Это правило завязано на изоморфизме hom-типов, поэтому оно также распространяется и на сопряжения — для любого функтора может быть лишь один сопряженный слева и лишь один сопряжённый справа. Многие функторы, связанные с категорией типов имеют оба сопряжения.

Характерным примером является диагональный функтор . Для декартово-замкнутых категорий (в т.ч. для категории типов) правым и левым сопряжением диагонального функтора будут предел и копредел соответственно. Это удобно представить в виде сопряжённой тройки:

Выберем некий . Построим вокруг него сопряжённую тройку с функторами . Это даст нам две пары эндофункторов для каждой категории:

Причём, в каждой паре для первого эндофунктора сопряжения дадут монаду, а для второго — комонаду.

Более того, каждая пара образует новое сопряжение:

Саму возможность их получения проще увидеть, рассматривая сопряжения как изоморфизмы hom-типов:

Из этой схемы можно вывести интересное следствие — алгебра монады изоморфна коалгебре комонады . То есть, буквально, если у вас есть «законопослушная распаковка» для , то вам автоматически доступна столь же хорошая «запаковка» , и наоборот. Аналогичное правило получается и для комонады с монадой .

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

Аналогично, для :

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

Более того, из выведенных только что сопряжений мы сразу получаем ещё две пары монад/комонад для композиций уже из четырёх функторов! В результате выстраивается такая цепочка:

• сперва мы имеем единственный функтор ;

• мы можем найти левый и правый сопряженный ему ;

• таким образом, получим сопряжённую тройку ;

• а из сопряжённой тройки автоматически получаются:

  • монады для эндофункторов

    • ;

    • ;

  • комонады для эндофункторов

    • ;

    • ;

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

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

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

Сопряжения на Scala

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

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

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

Для эндофункторов в категории типов и мы получим не особо интересные монады — они соответствуют редко используемым конструкторам типов [A] => A Either A и [A] => (A, A). Но можно попробовать декомпозировать на сопряжённые следующие эндофункторы:

type Result[E] = [A] =>> E + A
type Writer[L] = [A] =>> L × A

Впрочем, это не так-то просто сделать. Сопряжённые функторы для Result проходят через нетривиальную категорию косреза (coslice category), а в случае Writer промежуточная категория оказывается ещё сложнее (категория правых модулей моноида). И в обоих случаях сопряжённые функторы можно выразить лишь посредством зависимых типов. По указанным причинам не стану углубляться в эту тему, а выделю лишь главную идею:

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

На практике программисты могут встретиться с сопряжениями эндофункторов в категории типов. Давайте сперва посмотрим, как сопряжение представлено в программировании:

@targetName("Adjunction")
infix type ⊣[F[_], G[_]] = (
  η: Id ~> (G ∘ F),
  ε: (F ∘ G) ~> Id
)

inline def   unitAdj[F[_], G[_]](using adj: F ⊣ G) = adj.η
inline def counitAdj[F[_], G[_]](using adj: F ⊣ G) = adj.ε

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

infix type AdjHomIso[F[_], G[_]] = (
  left : [A, B] => (F[A] =>   B ) => (  A  => G[B]),
  right: [A, B] => (  A  => G[B]) => (F[A] =>   B ),
)

inline def  leftAdj[F[_], G[_]](using adjIso: AdjHomIso[F, G]) = adjIso.left
inline def rightAdj[F[_], G[_]](using adjIso: AdjHomIso[F, G]) = adjIso.right

Оба представления изоморфны, это можно продемонстрировать, предоставив такие встречные преобразования:

given [F[_], G[_]] => AdjHomIso[F, G] => F ⊣ G = (
  η = [A] => (a: A)         =>  leftAdj[F, G][A, F[A]](identity)(a),
  ε = [B] => (fgb: F[G[B]]) => rightAdj[F, G][G[B], B](identity)(fgb),
)

given [F[_]: Functor, G[_]: Functor] => F ⊣ G => AdjHomIso[F, G] = (
  left  = [A, B] => (fab: F[A] =>   B ) =>   unitAdj[F, G][A] andThen fmap[G](fab),
  right = [A, B] => (agb:   A  => G[B]) => counitAdj[F, G][B] compose fmap[F](agb),
)

Обратите внимание, для получение hom-изоморфизма из сопряжения уже явно требуются функториальные возможности F[_] и G[_], задействованные в методе def fmap[F[_]: Functor as lift] = lift.

Но самое, важное, из-за чего мы разбираем сопряжения, это возможность получения из них (ко)монад. Используя определения классов типов из предыдущей части обзора, можно записать так:

inline def id[F[_]]: F ~> F = [A] => (fa: F[A]) => fa // тождественное естественное преобразование

given [F[_]: Functor, G[_]: Functor] => F ⊣ G => Monad[G ∘ F] = (
  lift    = summon[Functor[G ∘ F]],        // призывается compFunctor
  pure    = unitAdj[F, G],                 // Id            ~> G ∘ F
  flatten = id[G] ∘ counitAdj[F, G] ∘ id[F] // G ∘ F ∘ G ∘ F ~> G ∘ F
)

given [F[_]: Functor, G[_]: Functor] => F ⊣ G => Comonad[F ∘ G] = (
  lift      = summon[Functor[F ∘ G]],       // призывается compFunctor
  extract   = counitAdj[F, G],              // F ∘ G ~> Id
  coflatten = id[F] ∘ unitAdj[F, G] ∘ id[G]  // F ∘ G ~> G ∘ F ∘ G ∘ F
)

Композиция функторов compFunctor определена ранее тут, а горизонтальная композиция естественных преобразований α ∘ β — тут.

Для раскрытия возможностей сопряжённых троек помогут такие композиции сопряжений:

given adjComp1: [F[_]: Functor, G[_]: Functor, H[_]: Functor] => F ⊣ G => G ⊣ H => (F ∘ G) ⊣ (H ∘ G) = (
  η = (id[H] ∘ unitAdj[F, G] ∘ id[G]) ⋅ unitAdj[G, H],
  ε = counitAdj[F, G] ⋅ (id[F] ∘ counitAdj[G, H] ∘ id[G])
)

given adjComp2: [F[_]: Functor, G[_]: Functor, H[_]: Functor] => F ⊣ G => G ⊣ H => (G ∘ F) ⊣ (G ∘ H) = (
  η = (id[G] ∘ unitAdj[G, H] ∘ id[F]) ⋅ unitAdj[F, G],
  ε = counitAdj[G, H] ⋅ (id[G] ∘ counitAdj[F, G] ∘ id[H])
)

Вертикальная композиция естественных преобразований α ⋅ β вводилась тут.

Давайте посмотрим, как это работает.

Контейнеры состояния и хранилища

Самый типичный пример, упоминаемый по данной теме в популярных источниках, это демонстрация и анализ сопряжения Writer[S] ⊣ Reader[S]. Давайте и мы сейчас это разберём, благо, само сопряжение реализуется очень просто:

type Writer[L] = [A] =>> L  ×  A
type Reader[R] = [A] =>> R  => A

given [L] => Functor[Writer[L]] = [A, B] => (f: A => B) => (wla: Writer[L][A]) => wla._1 -> f(wla._2)
given [R] => Functor[Reader[R]] = [A, B] => (f: A => B) => (rra: Reader[R][A]) => rra andThen f

given [S] => Writer[S] ⊣ Reader[S] = (
  η = [A] => (a: A) => (s: S) => s -> a,
  ε = [A] => (ssa: (S, S => A)) => ssa._2(ssa._1)
)

Связанный с сопряжением изоморфизм hom-функторов отражает простое алгебраическое соотношение:

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

Особый интерес представляют композиции этих функторов, для которых сопряжение даёт монаду и комонаду:

type State[S] = Reader[S] ∘ Writer[S] // S => (S, A)   монада
type Store[S] = Writer[S] ∘ Reader[S] // (S, S => A) комонада

Контейнер State[S] отвечает за извлечение значения A из неизвестного состояния s: S, при этом итоговое состояние может измениться. В свою очередь, Store[S] уже содержит некоторое состояние, и способ извлечения из него значения A. Значение a: A всегда можно запаковать в State[S][A], но не в Store[S][A], для которого требуется также состояние s: S. С другой стороны, у Store уже есть всё необходимое для распаковки A, в то время как для извлечения из State недостаёт s: S.

Оба композитных функтора имеют схожую семантику работы со значением A как малой части состояния S, но эти контейнеры, очевидно, не изоморфны. Cопряжение Writer[S] ⊣ Reader[S] даёт для них разные возможности — Monad[State] и Comonad[Store]. Собственно, различие между этими контейнерами как раз соответствует различным целям использования монад и комонад.

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

object State:
  def get [S] = (s: S) => s -> s             // в контейнере сохраняется переданное состояние
  def put [S] = (s: S) => (_:S) => s -> ()   // создаётся контейнер с пустым значнием, замещающий состояние
  def pure[S] = summon[Monad[State[S]]].pure // запаковка

extension [S, A](st: State[S][A])
  def runS = st andThen {_._1}         // вычисляем итоговое состояние
  def runA = st andThen {_._2}         // вычисляем итоговое значение
  def run  = st                        // вычисляем значение и состояние
  def modify(f: S => S) = f andThen st // изменяем состояние
  def inspect[B](f: S => B) = (s: S) => s -> f(s) // значение из состояния

Вот пример использования State для подсчёта изменений:

val f1: Double => State[Int][Double] = d => c => c + 1 -> (d + c) // увличиваем счётчик
val f2: Double => State[Int][String] = d => _ -> ("строка: " + d) // состояние не меняем
  
val resultEffect = State
  .pure(5.0)   // «запаковываем» 5.0
  .flatMap(f1) // увличиваем счётчик 1й раз
  .flatMap(f1) // увличиваем счётчик 2й раз
  .flatMap(f1) // увличиваем счётчик 3й раз
  .flatMap(f2) // счётчик не меняется

//старт счётчика ↓      ↓ итоговое состояние счётчика
resultEffect.run(0) // (3,строка: 8.0)
//                        ↑↑↑↑↑↑↑↑↑↑↑ итоговое значение

Контейнер Store[P][A] содержит позицию P и функцию вычисления значения A на основе позиции. Функция как раз и представляет собой хранилище значений A, индексированных позицией, а сам контейнер — это курсор, который знает своё «местоположение в хранилище значений»:

object Store:
  def apply[P, A](pos: P, peek: P => A): Store[P][A] = pos -> peek

extension [P, A](st: Store[P][A])
  def pos : P = st._1                                 // позиция
  def peek: A = summon[Comonad[Store[P]]].extract(st) // значение в позиции
  def seek (p: P)     : Store[P][A] =   p    -> st._2 // сдвигаем позицию
  def seeks(f: P => P): Store[P][A] = f(pos) -> st._2 // аналогично

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

val image = (i: Int, j: Int) => i + j // диагональный градиент
val initialStore = Store((0, 0), image.tupled)

def transform(store: Store[(Int, Int)][Int]): Int =
  val (i, j) = store.pos
  store.seek((i + j) % 8, (i * j) % 8).peek
//↑↑↑↑↑↑↑↑↑↑ используем другие значения из хранилища, но относительно текущей позиции

val finalStore: Store[(Int, Int)][Int] = initialStore.coflatMap(transform)

Метод transform имеет доступ ко всему изображению и к текущей позиции.

«Разматрёшивание» State[S] превращает два состояния в одно, что вместе с другими свойствами намекает на полезность возможностей моноида для S. В Store[P] хранимое значение однозначно представляет позиция P. Представимость контейнеров и моноиды для контекстов контейнеров характерны для любых сопряжённых функторов, и для построенных на их основе монад/комонад. В продолжении обзора мы рассмотрим эту особенность детальнее, так как она помогает строить композитные (ко)монады.

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

• Универсальные свойства и пределы.

  • Теория категорий на JavaScript. Часть 1. Категория множеств — безо всяких формул, но с помощью цветастых диаграмм раскрываются различные универсальные свойства на пальцах множествах.

  • Серия публикаций Бартоша Милевски из его блога:

    • Understanding Products and Universal Constructions

    • Programming with Universal Constructions

    • Limits and Colimits

    • Understanding Limits

  • Серия публикаций Тай-Данаэ Брэдли с ресурса Института Math3ma:

    • Limits and Colimits, Part 1 (Introduction)

    • Limits and Colimits, Part 2 (Definitions)

    • Limits and Colimits, Part 3 (Examples)

  • Understanding limits in Set — одна из самых «демократичных» среди прочих «математичных» статей на nLab.

• Сопряжения.

  • Из блога Милевски:

    • Adjunction

    • The power of adjunctions

  • Adjoint triples из блога Дана Дойля.

  • Повесть о стрелке и запятой — статья на Хабре о сопряжённых функторах в Haskell.

  • Adjoint Functors — оригинальная статья Даниеля Кана 1958 года.

  • Scala Comonad Tutorial, Part 2 — статья Рунара Бьярнасона из его блога.

• Приложение к программированию.

  • Adjunctions and Battleship — статья Криса Пеннера, демонстрирующая использование сопряжённых функторов для решении практических задач на Haskell.

  • State — описание монады State на сайте Typelevel Scala.

  • Comonads for Life — замечательная статья Джастина Хейеса-Джонса с примером применения в Scala комонады Store (там называется по-другому, но суть та же) для фильтрации изображений.

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

Тезисно:

• любой новый тип определяется путём описания его универсального свойства (мы предварительно знакомы с этим понятием);

• категориальное описание универсальных свойств выражается через понятия пределов и копределов функторов, причём, копредел даёт сумму типов, а предел — произведение (экспоненциал типов также можно представить как предел);

• сами (ко)пределы демонстрируют частный случай сопряжённых функторов — копредел является левым, а предел правым сопряжениями одного и того же диагонального функтора, отражающего простую идею выбора чего-то одного на основе какого-то набора;

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

• каждая пара сопряжённых функторов порождает монаду и комонаду;

• для заданного функтора его левое и правое сопряжения единственны с точностью до изоморфизма;

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

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

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