Категории типов. Часть 3. Естественные преобразования / Хабр

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

Данная публикация основана по большей части на посте Natural Transformations в блоге Бартоша Милевски.

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

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

Содержание

Условие естественности
Категория функторов
2-категория
Естественный изоморфизм
Промежуточный итог

Мотивация

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

val f: A => B = ???
val g: B => C = ???
val h: C => D = ???

val program: A => D = (a: A) => h(g(f(a))) // val program = h compose g compose f

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

Помимо преобразования между категориями морфизмов-функций, необходимо также преобразовывать и сами объекты. Проще говоря, нам нужны функции между объектами разных категорий. Для F-подкатегорий типов в общем случае это будут профункторы вида type ProfFG[A, B] = F[A] => G[B] и аналогичные им. Но с такими конструкциям не очень-то удобно работать. К профункторам мы ещё вернёмся в дальнейшем, а сейчас нам будет достаточно рассмотреть более простые функции:

infix type ~>[F[_], G[_]] = [X] => F[X] => G[X]

Это полиморфные функции, единообразно работающие для любого типа X — объекта категории типов. Например,

val lstToOpt: List ~> Option =
  [A] => (lstA: List[A]) => lstA.headOption

optToList(List(42)) // Some(42)

Оказывается, что не все такие функции одинаково полезны. Ранее мы уже рассматривали возможности функторов, переводящих морфизмы одной категории в другую, и в частности, функции A => B в F[A] => F[B]. Функторы позвол��ют существенно упростить программный код, и не хотелось бы упускать это преимущество. Однако, некоторые реализации преобразований вида F ~> G ведут себя «неестественно» по отношению к выбранным функторам, внося непредсказуемость в цепочки вычислений. Чтобы избежать таких проблем, необходимо ввести дополнительные законы, согласующие эти преобразования с функторами. Функции F ~> G, удовлетворяющие таким законам называются естественными преобразованиями.

Условие естественности

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

Красными волнистыми стрелками обозначены естественное преобразование для функторов и , а также его компоненты и — обычные морфизмы в категории — Красными волнистыми стрелками обозначены естественное преобразование $\alpha$ для функторов и , а также его компоненты $\alpha_a$ и $\alpha_b.$ — обычные морфизмы в категории $\mathcal{D}.$

Здесь стрелки и — это два разных функтора, действующих между категориями $\mathcal{C}$ и $\mathcal{D}$ . Функторы переводят морфизмы из исходной категории в разные морфизмы конечной. В категории $\mathcal{D}$ морфизмы образуют квадратный ориентированный граф, демонстрирующий наличие двух путей между $F\, a$ и $G\, b$ , отличающихся тем, когда именно применяется преобразование $\alpha$ — до или после «поднятого» морфизма .

Было бы здорово, если бы эта диаграмма коммутировала, то есть оба эти пути были одинаковыми. Ведь тогда, имея скомпозированный морфизм из $F\, a$ в $G\, b$ , не было бы причины уточнять, как он устроен, и его поведение было бы более предсказуемым.

Условие коммутативности данной диаграммы накладывается на преобразование $\alpha$ , которое в таком случае можно называть естественным по отношению к функторам и .

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

val f: A => B = ???

given   listFunctor: Functor[List  ] = [A, B] => (f: A => B) => (_: List  [A]).map(f) // встроенный метод
given optionFunctor: Functor[Option] = [A, B] => (f: A => B) => (_: Option[A]).map(f) // встроенный метод

val α: List ~> Option = [A] => (lstA: List[A]) => lstA.headOption                     // встроенный метод

val path1: List[A] => Option[B] = f.lift[Option] compose α[A]
val path2: List[A] => Option[B] = α[B] compose f.lift[List]

assert(path1(lstA) == path2(lstA)) // для любых lstA: List[A]

Если наше преобразование кристально чистое и универсально полиморфное, не гарантирует ли это его естественность автоматически (как это написано у Милевски)? На самом деле нет. Приведённое выше преобразование вполне себе естественно для пары функторов, представленных встроенными методами List.map и Option.map. Но если первый функтор заменить на darkFunctorList: Functor[List] из предыдущей части обзора, то естественность сразу теряется:

// если в контексте лежат darkFunctorList и обычный optionFunctor из предыдущего примера,
// тогда эти два пути уже не коммутируют!
val path1: List[String] => Option[Int] = f.lift[Option] compose α[String]
val path2: List[String] => Option[Int] = α[Int] compose f.lift[List]

val lstString = List("list", "42")

path1(lstString)  // Some(4)
path2(lstString)  // Some(2)

Для darkFunctor (в паре с Option.map) естественным будет такое тривиальное преобразование:

val β: List ~> Option = [A] => (_: List[A]) => None

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

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

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

val f: A => B = ???
val α: F ~> G = ???
//                                     было A ↓
val path1: F[A] => G[B] = f.lift[G] compose α[B] // требуется Contravariant[G]
val path2: F[A] => G[B] = α[A] compose f.lift[F] // требуется Contravariant[F]
//                          ↑ было B

assert(path1(fA) == path2(fA)) // для любых fa: F[A]

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

Категории функторов

Полиморфные функции F ~> G композируются между собой и с их помощью можно построить ещё одну категорию подкатегорий типов (используется класс типов Category, определённый в предыдущей части):

val cat: Category[~>] = (
  identity = [F[_]] => () =>
    [A] => (fa: F[A]) => fa,
  compose  = [F[_], G[_], H[_]] => (α: G ~> H, β: F ~> G) =>
    [A] => (fa: F[A]) => (α[A] compose β[A])(fa)
)

extension [H[_], G[_]] (α: G ~> H)(using cat: Category[~>])
  @targetName("verticalComposition")
  infix def ⋅[F[_]](β: F ~> G): F ~> H = cat.compose(α, β)

Cимвол ⋅ для композиции естественных преобразований позаимствован у МакЛейна (см. например, книгу «Категории для работающего математика»). Вот пример использования:

val idToList: Id   ~> List   = [A] => (a: A) => List(a)
val lstToOpt: List ~> Option = [A] => (lstA: List[A]) => lstA.headOption    
val idToOpt:  Id   ~> Option = lstToOpt ⋅ idToList

idToOpt(42) // Some(42)

Частным случаем F ~> G будут и естественные преобразования. Они также являются морфизмами в определённой только что категории, но любопытно то, что их ещё можно рассматривать в качестве морфизмов в категории функторов, действующих между двумя фиксированными категориями!

Действительно, рассмотрим такую диаграмму для $F,\,G,\,H:\: \mathcal{C} \rightarrow \mathcal{D}$ :

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

Здесь подразумевается, что прямоугольник $Fb\;Hb\;Ha\;Fa$ коммутирует — все пути от до эквивалентны. Преобразование $\alpha$ , заданное для функторов и , можно скомпозировать с $\beta$ , определённом для и , при этом получается преобразование $\alpha \cdot \beta$ между функторами и . Композиция получается ассоциативная и уважающая тождественное преобразование.

Объектами категории, основанной на такой композиции, являются все возможные функторы, но только между двумя фиксированными категориям. Например, категорию образуют все возможные значения эндофукнкторов Functor[F] для всех конструкторов типов F[_]. Hom-типы в таких категориях будут зависеть от значений-функторов, так что в данном обзоре мы обойдём эту тему.

2-категория

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

категории — 0-ячейки;
функторы — 1-ячейки (1-морфизмы);
естественные преобразования — 2-ячейки (2-морфизмы).

Это и привело к появлению нового термина — «2-категория». Если возникнет необходимость, то технически возможна и категория естественных преобразований с новым видом морфизмов (3-ячейки) и так далее по индукции. Идея в том, что на каждом (кроме нулевого) уровне иерархии объекты являются одновременно и морфизмами в предыдущей категории. В этом смысле уровни аналогичны друг другу, что упрощает работу с ними. Таким образом в теории категорий и появляются N-категории. В прочем, в программировании обычно достаточно только второго уровня.

«Богатство» 2-категории обусловлено взаимодействием морфизмов из разных уровней между собой. Например, выше мы уже видели, что 2-ячейки (естественные преобразования) могут выступать в качестве морфизмов между 0-ячейками (категориями конструкторов типов). А сейчас мы рассмотрим другие аспекты такого взаимодействия.

Пусть у нас есть две пары функторов $F,\, F': \mathcal{C} \rightarrow \mathcal{D}$ и $G,\, G': \mathcal{D} \rightarrow \mathcal{E}$ , а также пара естественных преобразований $\alpha: F \rightsquigarrow F'$ и $\beta: G \rightsquigarrow G'$ . Функторы первой пары приводят в категорию $\mathcal{D}$ , из которой исходят функторы второй пары. Следовательно, функторы из разных пар можно композировать между собой. Оказывается, что в таком случае можно построить такую «горизонтальную» композицию естественных преобразований $\beta \circ \alpha: G \circ F \rightsquigarrow G' \circ F'$ :

Горизонтальная композиция естественных преобразований.

Само же устройство горизонтальной композиции проще понять, если эту диаграмму развернуть так:

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

Здесь в середине мы получаем «волнистый квадрат» естественных преобразований c диагональю $\beta \circ \alpha$ . Эта диагональ отражает коммутативность квадрата — оба пути от $G \circ F$ к $G' \circ F'$ эквивалентны. Запись $G\, \alpha$ обозначает естественное преобразование $Id_G \circ \alpha$ , получаемое действием функтора на каждую компоненту-функцию $\alpha_a: F\, a \rightarrow F'\, a$ .

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

infix type ∘[G[_], F[_]] = [X] =>> G[F[X]]

extension[F1[_], F2[_]: Functor] (α: F1 ~> F2)
  @targetName("horizontalComposition")
  infix def ∘[G1[_], G2[_]](β: G1 ~> G2): (F1 ∘ G1) ~> (F2 ∘ G2) =
    [A] => (fga: (F1 ∘ G1)[A]) => (β[A].lift[F2] compose α[G1[A]])(fga)

При реализации нужен лишь один функтор. Здесь выбран «нижний» путь на квадрате, поэтому потребовался только Functor[G2]. Но всегда помним, что при работе с двумя естественными преобразованиями подразумевается наличие всех четырёх функторов.

Две разные композиции естественных преобразований называются «вертикальной» и «горизонтальной» от части потому, что они действуют в как бы «перпендикулярных измерениях», не влияя друг на друга. Композиции, как бинарные операции, удовлетворяют так называемому «обменному» (interchange) закону:

$(\alpha \cdot \beta) \circ (\alpha' \cdot \beta') =(\alpha \circ \alpha') \cdot (\beta \circ \beta')$

Это взаимоотношение естественных преобразований можно визуализировать так:

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

Естественный изоморфизм

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

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

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

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

assert((left  ⋅ right)(fa) == fa) // для любого типа A и значения fa: F[A]
assert((right ⋅ left )(ga) == ga) // для любого типа A и значения ga: G[A]

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

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

А вот в случае эндофункторов в категории типов картина интереснее — их естественный изоморфизм автоматически влечёт за собой изоморфизм соответствующих подкатегорий! Встречные функторы между подкатегориями (Hom[F, G], Hom[G, F]) строятся путём «подъёма» эндофункторами преобразований естественного изоморфизма. Эти функторы сразу получаются «взаимоуничтожающимися», что и даёт изоморфизм категорий.

В предыдущий части обзора через встречные функторы строился изоморфизм категорий для обобщённых типов

type Pair[X] = X × X
type Pow2[X] = Boolean => X  // X²

Покажем, что его гораздо проще продемонстрировать с помощью естественного изоморфизма соответствующих эндофункторов:

val туда   : Pow2 ~> Pair = [X] => (bx: Boolean => X) => bx(false) -> bx(true)
val обратно: Pair ~> Pow2 = [X] => (xx: (X, X)) => (b: Boolean) => if b then xx._2 else xx._1

assert((туда ⋅ обратно)(xx) == xx) // для любых xx: Pair[X]

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

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

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

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

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

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

Категории типов. Часть 3. Естественные преобразования