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

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

Оглавление обзора
  1. Hom-типы

  2. Функторы

  3. Естественные преобразования (данная публикация)

  4. (продолжение следует)

Содержание

Мотивация

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

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 для функторов F и G, а также его компоненты \alpha_a и \alpha_b. — обычные морфизмы в категории \mathcal{D}.

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

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

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

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

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 коммутирует — все пути от Fa до Hb эквивалентны. Преобразование \alpha, заданное для функторов F и G, можно скомпозировать с \beta, определённом для G и H, при этом получается преобразование \alpha \cdot \beta между функторами F и H. Композиция получается ассоциативная и уважающая тождественное преобразование.

Объектами категории, основанной на такой композиции, являются все возможные функторы, но только между двумя фиксированными категориям. Например, категорию образуют все возможные значения эндофукнкторов 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 обозначает естественное преобразование, получаемое действием функтора G на каждую компоненту-функцию \alpha_a: F\, a \rightarrow F'\, a.

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

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

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

При реализации нужен лишь один функтор. Здесь выбран «нижний» путь на квадрате, поэтому потребовался только 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]

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

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

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

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

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

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

Комментарии (0)