Категории типов. Часть 7½. Свободная монада

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

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

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

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

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

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

7½. Свободная монада
Композиция эффектов

Содеожание

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

Реализации расширений Кана

Возможности расширений Кана

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

Давайте посмотрим на экземпляры класса типов Functor[F[_]] для расширений Кана:

given ranFunctor: [F[+_], G[+_]] => Functor[F / G] =    [A, B] => (f: A => B) => (fga: (F / G)[A]) =>      [R] => (cont: B => G[R]) =>        fga(cont `compose` f)        //  ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑    given lanFunctor: [F[+_], G[+_]] => Functor[G \ F] =    [A, B] => (f: A => B) => (fga: (G \ F)[A]) =>      [R] => (cont: [X] => (G[X] => B) × F[X] => R) =>        fga([X] => (gxaFx: (G[X] => A) × F[X]) =>          cont(f `compose` gxaFx._1, gxaFx._2))          //   ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑

Чуть более сложный код для $\mathrm{Lan}_GF$ — неизбежная плата за работу с экзистенциальными (алгебраическими) типами данных.

Самое интересное то, что в обеих реализациях не задействована функториалность F[_] и G[_]. «Поднимаемая» функция f: A => B просто композируется либо с продолжением, либо внутри него. Такая особенность позволяет оптимизировать цепочки контейнерных вычислений для представлений Йонеды и монады коплотности, которые мы рассмотрим далее.

Единица и коединица наших расширений Кана реализуются очень просто, с использованием тождественной функции identity:

def εRan[F[+_], G[+_]]: (F / G) ∘ G ~> F =    [A] => ran => ran(identity[G[A]])  def ηLan[F[+_], G[+_]]: F ~> ((G \ F) ∘ G) =    [A] => (fa: F[A]) =>    [_] => cont => cont(identity[G[A]] -> fa)

Также крайне полезны универсальные свойства расширений, сопоставляющие произвольным кандидатам $(H, \alpha)$ такие универсальные естественные преобразования:

def uRan[F[+_], G[+_], H[+_]: Functor](α: H ∘ G ~> F): H ~> (F / G) =    [A] => (ha: H[A]) =>      [R] => (cont: A => G[R]) =>        α(fmap[H](cont)(ha))    def uLan[F[+_], G[+_], H[+_]: Functor](α: F ~> (H ∘ G)): (G \ F) ~> H =    [A] => (lana: (G \ F)[A]) => lana[H[A]](    [X] => gxaFx => fmap[H](gxaFx._1)(α(gxaFx._2))  )

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

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

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

$\begin{split} Fa \\ &\cong \int^c Fc \times \mathrm{Hom}(c,a) &&\equiv よ F a \\ &\cong \int_c \mathrm{Hom}\big(\mathrm{Hom}(a,c), Fc \big) &&\equiv よ^{op} F a. \end{split}$

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

В частности, для прямого представления Йонеды

type Yoneda[F[+_]] = F / Id // [A] =>> [X] => (A => X) => F[X]

ветви изоморфизма образуют единица расширения вместе с универсальным морфизмом кандидата $(H, \alpha)=(F, id_F)$ :

// тождественное естественное преобразование  inline def id[F[+_]]: F ~> F = [A] => identity[F[A]](_) // (fa: F[A]) => fa    def  liftYo[F[+_]: Functor]:        F  ~> Yoneda[F] = uRan[F, Id, F](id)  def lowerYo[F[+_]         ]: Yoneda[F] ~>        F  = εRan[F, Id]//  liftYo[F] ⋅ lowerYo[F] = id[F]// lowerYo[F] ⋅  liftYo[F] = id[Yoneda[F]]

Данный изоморфизм позволяет оптимизировать последовательность преобразований внутри контейнера F[_]:

переходим к представлению Йонеды Yoneda[F][_],
формируем цепочку из преобразований вида fmap[Yoneda[F]](f),
возвращаемся обратно к F[_].

Функториальность F[_] требуется уже на первом шаге «поднятия в мир Йонеды», но оно не применяется сразу, а сохраняется в «продолжении». Преобразования fmap[Yoneda[F]](f) не запускают это продолжение, а комбинируют с ним эти самые f — вся цепочка fmap просто добавляется к продолжению (fusion). И лишь единица расширения Кана запускает это продолжение вместе с изначально заложенным в него fmap[F]. Если F[_] представляет собой «тяжёлую» конструкцию (например, рекурсивная структура данных, вроде большого списка), то представление Йонеды позволит пробежаться по ней лишь раз в самом конце, а не на каждом шаге преобразований. В этом и заключается его оптимизационная сила.

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

Для представления ко-Йонеды имеем аналогичную картину:

type Coyoneda[F[+_]] = Id \ F    def  liftCoyo[F[+_]         ]:          F  ~> Coyoneda[F] = ηLan[F, Id]  def lowerCoyo[F[+_]: Functor]: Coyoneda[F] ~>          F  = uLan[F, Id, F](id)    //  liftCoyo[F] ⋅ lowerCoyo[F] = id[F]// lowerCoyo[F] ⋅  liftCoyo[F] = id[Coyoneda[F]]

Здесь также работает механизм оптимизации цепочек fmap, но в отличие от представления Йонеды, liftCoyo не требует наличия Functor[F]. Это означает, что мы можем строить цепочки контейнерных вычислений произвольного F[_] как полноценного функтора!

Представление ко-Йонеды позволяет отделить описание бизнес логики (цепочки контейнерных преобразований) от её интерпретации (lowerCoyo). И хотя в конце подразумевается необходимость экземпляра Functor[F], существует ещё и обходной манёвр переинтерпретации в другой полноценный функтор G[_]. Этот приём используется при работе со свободными монадами, и мы рассмотрим его позднее.

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

Другое замечательное расширение Кана, упоминавшееся ранее в обзоре, это правое расширение функтора вдоль себя:

type Codensity[F[+_]] = F / F // [a] =>> [x] => (a => F[x]) => F[x]

Его универсальное свойство позволяет определить монаду коплотности:

given codensityMonad: [F[+_]] => Monad[Codensity[F]] = (    fmap    = ranFunctor[F, F],    pure    = uRan[F, F, Id](id[F]),    flatten = uRan[F, F, (F / F) ∘ (F / F)]( // кандидат H = (F / F) ∘ (F / F)    εRan[F, F] ⋅ (id[F/F] ∘ εRan[F, F])    // α: H ∘ F ⇝ F = ε ⋅ (id_{F/F} ∘ ε)  )(using compFunctor[F / F, F / F])      // композиция функторов)

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

Монаду коплотности можно построить для произвольного функтора, но без дополнительных инструментов она практически бесполезна. Прежде всего, её не получится «распаковать» в отсутствие механизмов «запаковки/распаковки» функтора . Также недоступен «подъём» значений и морфизмов из F[_] в Codensity[F][_], если не предоставлено «разматрёшивание» F.

Но если предоставить для F[_] законопослушные монадные возможности, то можно реализовать такой изоморфизм:

def  liftCodens[F[+_]: Monad     ]: F ~> Codensity[F] = [A] => (fa: F[A]) => [X] => fa.flatMap(_)  def lowerCodens[F[+_]: Monad as F]: Codensity[F] ~> F = [A] => _(F.pure[A])//  liftCodens[F] ⋅ lowerCodens[F] = id[F]// lowerCodens[F] ⋅  liftCodens[F] = id[Codensity[F]]

В отличие от представлений Йонеды, здесь мы имеем изоморфизм монад, а не просто функторов.

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

Вторая упоминалась в шестой части обзора — идея заключается в том, что механизм продолжений как бы «обращает последовательность flatten», опираясь на монадный закон ассоциативности. Цепочка «разматрёшиваний», соответствующая многократному пробеганию тяжёлой структуры F[_] «в ширину», превращается в однократное пробегание «в глубину» без размещения в памяти промежуточных результатов. В результате, квадратичная сложность (по количеству «разматрёшиваний») становится линейной.

Монада коплотности помогает вычислять свободные объекты, в частности, свободные монады как начальные алгебры функторов (начальный объект категории F-алгебр).

Свободная монада функтора

Определение

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

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

Поэтому обычно монада $(T, \eta, \mu)$ строится для заведомо «хорошего» эндофунктора $T\colon \mathcal{C} \to \mathcal{C}$ , основанного на заданном $F\colon \mathcal{C} \to \mathcal{C}$ , со встроенной возможностью «подъёма» значений $lift\colon F \rightsquigarrow T$ . Это позволяет поднимать отдельные операции вида $a \to Fb$ в $a \to Tb$ и уже там строить из них цепочки монадных вычислений.

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

эндофунктору сопоставляется такая монада $(T, \eta, \mu)$ с преобразованием $lift\colon F \rightsquigarrow T$ , что для любого преобразования $\alpha\colon F \rightsquigarrow M$ в любую монаду-кандидат существует единственный (универсальный) морфизм $u\colon T \rightsquigarrow M$ , такой что $\alpha = u \cdot lift$ .

Реализация на основе универсального свойства

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

$T = U \circ \tilde F = U \circ (Id/U) \cong U/U= \mathrm{Codens}\, U,$

где $\tilde F = Id/U \dashv U$ — свободный функтор для забывающего некоторой промежуточной категории. И, пожалуй, самой важной для нашего случая будет категория монад $\mathrm{Mon}(\mathcal{C})$ с объектами $(M,\eta,\mu)$ и забывающим функтором $U_M: \mathrm{Mon}(\mathcal{C}) \to \mathrm{Endo}(\mathcal{C})$ в категорию эндофункторов $\mathrm{Endo}(\mathcal{C})=\mathcal{C}^\mathcal{C}$ . Тогда, учитывая действие забывающего функтора $U_M(M,\eta,\mu) = M$ , запишем такой эндофунктор в категории эндофункторов:

$\begin{split} &\mathrm{Free} \colon \mathrm{Endo}\big(\mathcal{C}\big) \to \mathrm{Endo}(\mathcal{C}) = \mathrm{Codens}\, U_M, \\ &\mathrm{Free}\, F\, a = \int_{(M,\eta,\mu):\,\mathrm{Mon}(\mathcal{C})} \big(F \rightsquigarrow M\big) \to M a. \end{split}$

По сути это ни что иное, как воплощение универсального свойства свободной монады. Такой конец даёт нам одну из самых простых программных реализаций:

type FreeU[F[_]] = [X] =>> [M[_]] => Monad[M] ?=> (F ~> M) => M[X]    given freeUFunctor: [F[_]] => Functor[FreeU[F]] =    [A, B] => (f: A => B) => (fa: FreeU[F][A]) =>      [M[_]] => (M: Monad[M]) ?=> (interpreter: F ~> M) =>        fa(interpreter).map(f)    given freeUMonad: [F[_]] => Monad[FreeU[F]] = (    fmap    = freeUFunctor,    pure    = [A] => (a: A) => [M[_]] => (M: Monad[M]) ?=> (_: F ~> M) => M.pure(a),    flatten = [A] => (ffa: FreeU[F][FreeU[F][A]]) =>      [M[_]] => (M: Monad[M]) ?=> (interpreter: F ~> M) =>        ffa(interpreter).flatMap(_(interpreter))  )    def liftFreeU[F[_]]: F ~> FreeU[F] =    [A] => (fa: F[A]) =>      [M[_]] => (_: Monad[M]) ?=> (interpreter: F ~> M) =>        interpreter(fa)    inline def foldMapU[F[_], M[_]: Monad as M]: (F ~> M) => (FreeU[F] ~> M) =    interpreter => [A] => (fa: FreeU[F][A]) => fa(interpreter)

Здесь мы видим истинно универсальную свободную монаду:

самая простая чисто функциональная реализация с использованием техники передачи продолжений;
линейная сложность монадной композиции по количеству шагов;
в коде нет явной зависимости от Functor[F] — она прячется только в преобразовании interpreter: F ~> M, обеспечивая его «естественность».

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

Рекурсивные реализации

Вывод формул

Родство функторов и легче заметить, переписав универсальное свойство свободной монады через изоморфизм естественных преобразований: $\mathrm{Hom}\, (F, M) \cong \mathrm{Hom}\, (T, M)$ . Но более важно, что из этого изоморфизма, справедливого для любого M, следует изоморфизм категорий алгебр функтора и алгебр монады:

Здесь \mathcal{Alg}_F — это категория F-алгебр, объектами которой выступают пары (a, \alpha), где «распаковка» \alpha: Fa \to a согласуется с функториальностью. В свою очередь, \mathcal{Alg}_T представляет собой категорию алгебр Эйленберга-Мура монады T (см. предыдущую часть обзора). По структуре она очень похожа категорию aлгебры функтора, но более ограничена ввиду того, что «распаковки» и морфизмы между ними обязаны подчиняться законам монады.

$\mathcal{Alg}_F \cong \mathcal{Alg}_T.$

Через категорию алгебр Эйленберга-Мура $\mathcal{Alg}_T$ проходит ещё одно важное сопряжение, порождающее монаду. И пользуясь изоморфизмом категорий алгебр, мы можем выразить искомый функтор через забывающий функтор $U_F\colon \mathcal{Alg}_F \to \mathcal{C}$ из известной категории F-алгебр: $T = \mathrm{Codens}\,U_F$ .

Давайте найдём значение этого функтора в точке $x: \mathcal{C}$ , с помощью исчисления концов. Подставим полученное в предыдущей части обзора явное выражение правого расширения Кана в виде конца и учтём, что забывающий функтор действует на объекты категории F-алгебр как $U_F(a,\alpha)=a$ . Тогда конец по категории F-алгебр, представляющий монаду коплотности, можно переписать так:

$\begin{split} T\, x &\cong\int_{(a, \alpha)\colon \mathcal{Alg}_F} \mathrm{Hom}\big(\mathrm{Hom}(x, a), a\big) \\ &\cong \int_{(a, \alpha)}\int_{f: \mathrm{Hom}(x, a)} a \cong \int_{\big((a, \alpha), f\big):\, x \downarrow U_F} a. \end{split}$

Сперва мы под интегралом переписали экспоненциал через конец в дискретной категории функций $f: \mathrm{Hom}(x, a)$ , а затем объединили два интеграла в конец по категории запятой $x \downarrow U_F$ .

Ключевой момент: такая категория запятой с объектами $\big((a, \alpha), f\big)$ изоморфна категории алгебр $\mathcal{Alg}_{\dot F}$ функтора $\dot F_x\, a = x + Fa$ с объектами $\big(a, (f, \alpha)\colon x + Fa \to a\big)$ — структура морфизмов у них также одинакова. Это позволяет преобразовать конец по категории запятой в конец по категории $\dot F_x$ -алгебр. Преимущество такого подхода в том, что забывающий функтор $U_{\dot F_x}$ сохраняет пределы и можем вынести его за знак интеграла:

$T\, x \cong \int_{b\colon\, \mathcal{Alg}_{\dot F_x}} U_{\dot F_x} b \cong U_{\dot F_x}\int_{b\colon\, \mathcal{Alg}_{\dot F_x}} b \cong U_{\dot F_x}\lim_{\mathcal{Alg}_{\dot F_x}} Id.$

Как известно, предел тождественного функтора даёт начальный объект категории. В нашем случае это будет начальная алгебра $(i_x, \alpha_{i_x}\colon \dot F_x i_x \to i_x)$ и забывающий функтор $U_{\dot F_x}$ возвращает её носитель . В результате получаем, что

функтор свободной монады для в точке — это носитель начальной алгебры функтора $\dot F_x\, a = x + Fa$ .

Важной особенностью носителя начальной алгебры эндофунктора является то, что он является неподвижной точкой этого функтора: $Gi \cong i$ (вправо ведёт алгебра $\alpha_i\colon Gi \to i$ , а стрелка влево получается из универсального свойства начального объекта). Для обозначения неподвижной точки функтора $G\colon \mathcal{C} \to \mathcal{C}$ определим такой функтор $\mu\colon \mathcal{C}^\mathcal{C} \to \mathcal{C}$ , что $\mu G = i$ . Тогда свободная монада в точке будет такой:

$\begin{split} T x &=\mu \dot F_x \\ &= x + F (T x). \end{split}$

Эти равенства дают ещё две программные реализации свободной монады.

Реализация через неподвижную точку

Одна из реализаций неподвижной точки следует из определения свободной монады через конец для монады коплотности:

$\begin{split} T x &= \mu \dot F_x \\ &\cong\int_{(a, \alpha)\colon \mathcal{Alg}_F} \mathrm{Hom}\big(\mathrm{Hom}(x, a), a\big) \\ &\cong \int_{a}\mathrm{Hom}\Big(\mathrm{Hom}(Fa, a),\,\mathrm{Hom}\big(\mathrm{Hom}(x, a), a\big)\Big) \\ &\cong \int_{a}\mathrm{Hom}\big(\mathrm{Hom}(\dot F_x a, a),\, a \big). \end{split}$

Здесь мы сперва разобрали исходной двойной интеграл и преобразовали конец по $\alpha\colon \mathrm{Hom}(Fa, a)$ в экспоненциал (дополнительный $\mathrm{Hom}$ ), а затем чисто алгебраически преобразовали подинтегральное выражение.

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

$\mu G = \int_a\mathrm{Hom}\big(\mathrm{Hom}(G a, a),\, a \big).$

Это очень похоже на естественное преобразование из алгебры $\mathrm{Hom}(G a, a)$ в тождественный функтор . Но не более чем «похоже» — конструкция $\mathrm{Hom}(G a, a)$ инвариантна по , так что это преобразование просто не может быть «естественным». Благо в программировании реализация такого преобразования не требует функториальности, что позволяет записать свободную монаду следующим образом:

type Algebra[G[_]] = [A] =>> G[A] => A // Hom(Ga, a)type μ[G[_]] = Algebra[G] ~> Id // «псевдоестественное» преобразованиеtype Pointed[F[_], X] = [A] =>> X + F[A]    // Ḟₓtype Freeμ[F[_]] = [X] =>> μ[Pointed[F, X]] // μ Ḟₓgiven freeμFunctor: [F[_]] => Functor[Freeμ[F]] =    [A, B] => (f: A => B) => (fa: Freeμ[F][A]) =>      [X] => (alg: Algebra[Pointed[F, B]][X]) => fa:        case Left(a)   => alg(Left(f(a)))        case Right(fx) => alg(Right(fx))    given freeμMonad: [F[_]] => Monad[Freeμ[F]] = (    fmap    = freeμFunctor,    pure    = [A] => (a: A) => [X] => (alg: Algebra[Pointed[F, A]][X]) => alg(Left(a)),    flatten = [A] => (ffa: Freeμ[F][Freeμ[F][A]]) =>      [X] => (alg: Algebra[Pointed[F, A]][X]) => ffa[X]:        case Left(fa)  => fa(alg)        case Right(fc) => alg(Right(fc))  )def liftFreeμ[F[_] : Functor]: F ~> Freeμ[F] =  [A] => (fa: F[A]) =>    [X] => (alg: Algebra[Pointed[F, A]][X]) =>        alg(Right(fa.map(a => alg(Left(a)))))    def foldMapμ[F[_], M[_]: Monad as M]: (F ~> M) => (Freeμ[F] ~> M) =    interpreter => [A] => (fa: Freeμ[F][A]) => fa:      case Left(a)    => M.pure(a)      case Right(fma) => M.flatten(interpreter(fma))

Подробнее о программировании неподвижных точек функторов было рассказано в обзоре рекурсивных типов.

GADT-реализация

Равенство представляет собой рекурсивное определение свободной монады, которое более привычно программистам:

enum Free[F[_], A]:    case Pure(a: A)                   // первое  слагаемое   case Suspend(ffa: F[Free[F, A]])  // воторое слагаемое    def map[B](using Functor[F])(f: A => B): Free[F, B] =      this match        case Pure(a)     => Pure(f(a))        case Suspend(fa) => Suspend(fa.map(_.map(f)))      def flatMap[B](using Functor[F])(f: A => Free[F, B]): Free[F, B] =      this match        case Pure(a)     => f(a)        case Suspend(fa) => Suspend(fa.map(_.flatMap(f)))      // универсальное свойство свободной монады: (F ~> M) => (Free[F] ~> M)    def foldMap[M[_]: Monad as M](interpreter: F ~> M): M[A] =      this match        case Pure(a)     => M.pure(a)        case Suspend(fa) => interpreter(fa).flatMap(_.foldMap(interpreter))

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

Существенным недостатком такой GADT-реализации Free является квадратичная сложность композиции монадных вычислений. Поэтому именно в этом виде свободные монады на практике не встречаются.

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

Функториальность представленного выше Free[F] завязана на функториальность самого F. Тип Freeμ[F] требует Functor[F] лишь в преобразовании «подъёма» liftFreeμ: F ~> Freeμ[F], но в обоих случаях для композиции эффективных вычислений A => F[B] через эти свободные монады не обойтись без предоставления функториальности F.

Ранее уже говорилось, этот шаг можно отложить «на потом», обернув F в представление ко-Йонеды. Вот что получается в результате:

type Freerμ[F[+_]] = [X] =>> μ[Pointed[Coyoneda[F], X]]    given freerμFunctor: [F[+_]] => Functor[Freerμ[F]] =    [A, B] => (f: A => B) => (fa: Freerμ[F][A]) =>      [X] => (alg: Algebra[Pointed[Coyoneda[F], B]][X]) => fa:        case Left(a) => alg(Left(f(a)))        case Right(fx) => alg(Right(fx))    given freerμMonad: [F[+_]] => Monad[Freerμ[F]] = (    fmap = freerμFunctor,    pure = [A] => (a: A) => [X] => (alg: Algebra[Pointed[Coyoneda[F], A]][X]) => alg(Left(a)),    flatten = [A] => (ffa: Freerμ[F][Freerμ[F][A]]) =>      [X] => (alg: Algebra[Pointed[Coyoneda[F], A]][X]) => ffa[X]:        case Left(fa) => fa(alg)        case Right(fc) => alg(Right(fc))  )    def liftFreerμ[F[+_]]: F ~> Freerμ[F] =    [A] => (fa: F[A]) => [C] => alg =>      alg(Right(        [R] => (cont: [X] => ((X => C, F[X])) => R) =>          cont[A](a => alg(Left(a)), fa)      ))  def foldMapμ[F[+_], M[_] : Monad as M]: (F ~> M) => (Freerμ[F] ~> M) =    interpreter => [A] => (fa: Freerμ[F][A]) => fa:      case Left(a) => M.pure(a)      case Right(co) => co[M[A]]([X] => (pair: (X => M[A], F[X])) =>        interpreter(pair._2).flatMap(pair._1)      )

В реализации liftFreerμ мы воспользовались основной фишкой ко-Йонеды и теперь ни один метод не требует явного наличия Functor[F]. (Хотя он неявно присутствует в преобразовании interpreter: F ~> M, обеспечивая его «естественность»).

Представление ко-Йонеды выражается через ко-конец, то есть, через сумму типов. Это буквально означает, что в GADT-реализации второй конструктор Suspend теперь будет параметризирован дополнительным типом X, по которому и производится суммирование в ко-Йонеде:

enum Freer[F[_], A]:    case Pure(a: A) //    ↓↓↓↓↓ Coyoneda[F][Freer[F, A]] ↓↓↓↓↓  case Suspend[F[_], A, X](fx: F[X], cont: X => Freer[F, A]) extends Freer[F, A]      def map[B](f: A => B): Freer[F, B] =      this match        case Pure(a)           => Pure(f(a))        case Suspend(fx, cont) => Suspend(fx, cont(_).map(f))      def flatMap[B](f: A => Freer[F, B]): Freer[F, B] =      this match        case Pure(a)           => f(a)        case Suspend(fx, cont) => Suspend(fx, cont(_).flatMap(f))      def foldMap[M[_]: Monad as M](interpreter: F ~> M): M[A] =      this match        case Pure(a)           => M.pure(a)        case Suspend(fx, cont) => interpreter(fx).flatMap(cont(_).foldMap(interpreter))

Конструктор Suspend «запоминает» продолжение вычислений cont: X => Freer[F, A], откладывая сам процесс «на потом». В методах map и flatMap это продолжение лишь дополняется, и только в foldMap производится рекурсивное вычисление.

Обратите внимание: механизм продолжений, заложенный в представление ко-Йонеды позволил упростить квадратичную сложность монадной композиции во Free до линейной во Freer. И всё же, в современных библиотеках предпочитают более ленивые реализации свободной монады, нацеленные на интроспекцию и оптимизацию полной цепочки вычислений.

Свободная монада в библиотеках

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

$\begin{split} lift & \colon & F \rightsquigarrow T, \\ \eta & \colon & Id \rightsquigarrow T, \\ \mu & \colon & \,T \circ T \rightsquigarrow T. \end{split}$

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

$T = Id + F + T \circ T.$

Обычно стремятся получить наиболее широкую сумму с использованием продолжений. В этих целях разберём внешний контейнер композиции $T \circ T$ в виде суммы через лемму ниндзя-ко-Йонеды: $Ta \cong \int^x Tx \times \mathrm{Hom}(x, a)$ и под интегралом подставим Ta вместо a. Получается такая конструкция:

$Ta = a + Fa + \int^x Tx \times \mathrm{Hom}(x, Ta).$

Именно эта формула реализуется в различных библиотеках. Например, в Cats свободная монада описывается конструкцией вида

enum Free[F[_], A]:    case Pure(a: A)    case Suspend(fa: F[A])    case FlatMapped[F[_], A, X](fx: Free[F, X], f: X => Free[F, A]) extends Free[F, A]

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

В частности, полезно посмотреть как в cats при свёртке foldMap (а также run и т.п.) осуществляется обработка одного шага:

  /**   * Takes one evaluation step in the Free monad, re-associating left-nested binds in the process.   */  @tailrec  final def step: Free[S, A] =    this match {  //                          ↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓      case FlatMapped(FlatMapped(c, f), g) => c.flatMap(cc => f(cc).flatMap(g)).step      case FlatMapped(Pure(a), f)          => f(a).step      case x                               => x    }

Стрелками отмечено место, где осуществляется оптимизация путём переассоциации последовательности преобразований: пара шагов «схлопывается» сразу, без пробегания всей последовательности. Хвостовая рекурсия в step превращает свободную монаду в батут (trampoline), что позволяет использовать её для обеспечения стекобезопасности любой рекурсии.

В библиотеке Scalaz свободная монада устроена аналогичным образом.

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

Представления Йонеды:
- Yoneda — статья на сайте EuclideanSpace Мартина Бейкера даёт чисто категориальное объяснение вложений Йонеды с использованием большого количества кратинок
- The Yoneda Lemma: What’s It All About? pdf-статья Тома Лейнстера
- Из Кафе программирования Бартоша Милевски:
  - Yoneda Embedding
  - The Yoneda Lemma
Монада коплотности:
- Where Do Monads Come From? статья Тома Лейнстера из его Кафе n-Категории
Свободная монада
- Из блога The Comonad.Reader Эдварда Кметта
- Из блога Higher order Рунара Бьярнасона
  - Free Monads and the Yoneda Lemma
  - Free Monoids and Free Monads
- Stack Safety for Free pdf-статья Фила Фримена
- FreeR — Hybrid Free Monads for Reduced Quadratic Complexity/Observability & Map-Fusion Optimization in Scala статья Паскаля Войто из Мандубийского блога — измерения производительности более свободной монады Freer

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

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

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

Free[() => *, _] представляют собой батуты, вроде TailRec из стандартной библиотеки, Trampoline из Scalaz или Eval из Cats;
Free[Async, _], где под Async подразумевается контейнер для параллельных вычислений, реализуется в различных универсальных монадах ввода-вывода IO;
рекурсивные структуры данных, являющиеся монадами, изоморфны свободным монадам простых конструкторов типов, например, List[A] ≅ Free[(A, *), Unit].

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

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