Предисловие

Я много лет программировал на C# — популярном объектно-ориентированном языке программирования. Изучил ООП-шные паттерны, детально разобрал SOLID и другие принципы разработки. Успешно применял всё это на практике и был вполне доволен собой. Во только не давали покоя вопросы вроде «как развивать навыки программирования дальше?», «это что, предел?», «пора искать более интересную профессию?». Но возращение в науку (теоретическая физика) выглядело для меня совсем уж бесперспективным…

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

Будучи закоренелым ООП-шником, я тогда с большим скепсисом относился к функциональной парадигме, хотя и слышал, что такое крутое нововведение в C#, как Linq, позаимствовано именно оттуда. А про теорию категорий я не знал вообще ничего. Заглянул в Википедию — совсем не впечатлило — подумаешь, какие-то бесполезные стрелочки! В итоге забыл об этом на некоторое время.

Однако, меня зацепила сама идея познакомиться с ФП поближе. Начал, конечно же, с ресурса Скотта Влашина F# for Fun and Profit… Знаю, прозвучит банально, но для меня открылся новый мир! Я буквально прозрел и раздвинул горизонты собственного невежества. «Так вот что это такое — программирование!»

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

Также мне повсеместно стали бросаться в глаза функторы с монадами (IEnumrable, Nullable, Task…), хотя на тот момент я весьма поверхностно представлял себе, что же на самом деле стоит за этими терминами и насколько широки возможности их применения. Моей целью стало исследовать этот вопрос, найти за слоями «сложной» математики тот самый простой минимальный базис, на котором основываются все «лучшие практики» программирования.

Сперва я познакомился с основами -исчисления, теории типов и математической логики, а вскоре руки дошли и до пресловутой теории категорий — именно тут и появляются все эти функторы-монады. Основным источником сведений стали публикации Бартоша Милевски, из части которых составлена книга Category Theory for Programmers (переводы нескольких глав этой книги опубликованы на Хабре).

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

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

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

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

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

Некоторые темы были освещены ранее в предыдущих обзорах:

• Теория типов.

• Обобщённые типы.

• Рекурсивные типы.

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

Для примеров кода я использую язык программирования Scala. Это весьма компромиссный язык, одной из целей которого является упрощение переучивания программистов с популярных императивных языков на функциональное программирование. Ведь на Scala можно программировать как по старинке, чисто в стиле «better Java», так и в самых продвинутых функциональных стилях. К сожалению, эта вариативность Scala является её же минусом. Синтаксис языка, помимо относительно лёгких «функциональных» возможностей, несёт и громоздкое ООП-шное наследие. Программы, написанные на Scala, работают в объектно-ориентированной среде JRE, да и вообще вся «функциональщина» тут реализована через ООПу. В этом смысле язык Scala оказывается заметно сложнее своих конкурентов.

Тем не менее, считаю, что для демонстрации фундаментальных концепций передовых техник программирования лучше всего подходит именно синтаксис Scala. Даже устаревающий Haskell, с его ML-синтаксисом, близким к -исчислению, зачастую уступает в выразительных возможностях. Да и по популярности среди ФП-языков Scala занимает лидирующие позиции. Поэтому в своих обзорах использую именно его.

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

Категория

Мотивация

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

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

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

Полный путь определяется совокупностью отдельных шагов, каждый из которых по сути также является «маленьким путём». Это значит, что нужно уметь строить новые пути как композицию известных. Построение большого пути из маленьких само по себе является вычислением, каждым шагом которого является комбинирование двух путей в один. Для каждого типа у нас есть тривиальный путь — функция identity[A]: A => A. Кроме того, так как пути являются независимыми и равноправными, комбинировать смежные можно в любом порядке — в итоге получится один и тот же полный путь. Следовательно, операция комбинирования путей обязана быть ассоциативной.

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

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

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

Определение

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

Категория — это

• объекты

• морфизмы (отношения, «стрелки») между объектами, причём,

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

  • определена операция композиции между присоединёнными морфизмами, которая

    • ассоциативна и

    • сохраняет исходный морфизм при композиции с тождественным (как слева, так и справа).

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

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

1. по чёрным стрелкам — сначала f, потом g и в конце h;

2. сначала f, потом композиция h ∘ g;

3. сначала композиция g ∘ f, потом h;

4. композиция h ∘ g ∘ f.

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

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

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

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

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

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

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

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

Примеры категорий

Основная категория типов

Самая важная для программирования категория состоит из следующих компонентов:

• объекты — это типы (внимание! не значения типов, а сами типы!),

• морфизмы — функции между типами,

  • тождественный морфизм — встроенная функция identity[A],

  • композиция морфизмов — встроенные функции Function1.compose, или Function1.andThen,

    • которые, естественно, ассоциативные

    • и «уважают» identity.

Далее такую категорию мы будем называть основной.

Так или иначе, все пути программы начинаются и оканчиваются в этой категории. Её основные свойства определяются hom-типом Function1[A, B] и его встроенными возможностями:

type Hom = [A, B] =>> A => B

val morphism1: Hom[Double, String] = _.toString  
val morphism2: Hom[String, Int   ] = _.length  
  
val morphism3: Hom[Double, Int   ] = morphism1 andThen identity[String] andThen morphism2  
val morphism4: Hom[Double, Int   ] = morphism2 compose morphism1 compose identity[Double]
  
// функции morphism3 и morphism4 эквивалентны!
morphism3(42.0)) // 4  
morphism4(42.0)) // 4

В данном примере функции morphism3 и morphism4 хоть и отличаются с точки зрения JRE, но на самом деле являются эквивалентными. В случае, когда hom-тип является типом функции, продемонстрировать эквивалентность его значений-морфизмов задача не простая. Честное доказательство потребовало бы перебрать все различные значения исходного типа-объекта и убедиться, что в каждом случае значения результатов совпадают. Очевидно, это возможно далеко не всегда, поэтому эквивалентность данных путей предлагаю принять на веру)).

Дискретная категория

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

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

type Hom = [A, B] =>> A match
  case B => Nothing => (Nothing & A)
  case _ => Nothing

extension [A] (id: Hom[A, A])
  infix def compose(sameId: Hom[A, A]): Hom[A, A] = id

def identity[A]: Hom[A, A] = scala.Predef.identity[Nothing]

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

summon[Hom[Int, String] =:= Nothing            ]
summon[Hom[Int, Int]    =:= Hom[String, String]] // ошибка компиляции!

val sameIdentity = identity[Int] compose identity[Int]  
val ridiculous   = identity[Int] compose identity[String] // ошибка компиляции!

Кстати оператор =:= в этом примере представляет собой совершенно аналогичный морфизм для дискретной категории типов. То есть, hom-тип вполне можно было бы определить так: type Hom = [A, B] =>> A =:= B.

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

sealed trait Hom(a: Any, b: Any):
  infix def compose(other: Hom): Hom = if this == other then this else ???
final case class identity(o: Any) extends Hom(o, o)

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

val f = identity(42)
val g = f compose f

assert(f == g)           // проверка времени исполнения
f compose identity("42") // выбросит исключение!

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

Категория подтипизации

По аналогии с дискретными категориями типов вполне можно определить и категории порядка. Например, можно определить категорию с морфизмами-подтипизацией:

type Hom = [A, B] =>> A <:< B

def identity[A]: Hom[A, A] = summon[A <:< A]

val f: Hom[String , Any   ] = summon[String  <:< Any   ]
val g: Hom[Nothing, String] = summon[Nothing <:< String]
val h: Hom[Nothing, Any   ] = f compose g

Обобщённый класс <:<[-From, +To] определён в стандартной библиотеке Scala как наследник функции From => To. Наследование отражает простой факт, что отношение подтипизации — это не более чем функция (неявного) приведения значения одного типа к другому.

Категория с одним объектом

Что будет, если использовать Hom-тип, который вообще не зависит от типов-параметров?

type Hom = [A, B] =>> Int

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

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

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

Функция compose, работая с мономорфными типом Hom представляет собой обычную бинарную операцию (Hom, Hom) => Hom. Законы композиции морфизмов (ассоциативность и свойства identity) делают из этой бинарной операции моноид.

Моноид на целых числах можно реализовать по-разному, например, посредством сложения:

extension (f: Hom)
  infix def compose(g: Hom): Hom = f + g
val identity: Hom = 0

val f: Hom = 20
val g: Hom = 22
val h: Hom = f compose identity compose g // 42

А можно и через умножение:

extension (f: Hom)
  infix def compose(g: Hom): Hom = f * g
val identity: Hom = 1
  
val f: Hom = 7
val g: Hom = 6
val h: Hom = f compose identity compose g // 42

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

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

object identity
type Hom = identity.type
extension (f: Hom)
  infix def compose(g: Hom): Hom = f
  
assert(identity compose identity eq identity)

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

Ещё одна похожая категория

Конструкторы типов F[_] также можно рассматривать как морфизмы. Тождественный морфизм и композиция задаются очевидным образом:

type Id[A] = A
infix type ∘[F[_], G[_]] = [X] =>> F[G[X]]
// (IO ∘ Id ∘ Option)[A] = IO[Option[A]]

Конечно же, эта композиция ассоциативна.

Hom-типом в данном случае является вид обобщённых типов: . Такие конструкторы типов являются отображением простых типов в них же. Таким образом, это морфизмы в категории с единственным объектом — видом простых типов .

Класс hom-типов

Чтобы собрать воедино общие свойства разных категорий типов, выразим их с помощью класса hom-типов. Вот как это может выглядеть:

type Category[->[a, b]] = (
  identity: [A]       => ()               => A -> A,
  compose : [A, B, C] => (B -> C, A -> B) => A -> C
)

Значения Category предоставляют для некоторого двухпараметрического hom-типа -> пару функций — тождественный морфизм и композицию. Тождественный морфизм identity описан как функция из () из-за ограничений Scala, не разрешающих использовать полиморфные значения.

Также добавим щепотку синтаксического сахара:

extension [A, B, ->[_, _]: Category as cat](morph: A -> B)
  inline infix def ∘[C](prevMorph: C -> A): C -> B = cat.compose(morph, prevMorph)
  
inline def identity[->[_, _]: Category as cat, A] = cat.identity[A]()

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

В библиотеке Cats представлен аналогичный класс типов. Кстати, если вдруг кто-то из читателей ещё не знает)), само название этой популярной библиотеки посвящено не столько известному мему про выпас кошек, сколько именно теории категорий (Categories).

F-подкатегории типов

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

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

В программировании часто встречаются категории, объектами которых считаются типы F[A], для некого конструктора типов F[_], морфизмы — обычные функции между ними. Хотя для определения F-категории это вовсе не обязательно, обычно F полагается ковариантным, и это позволяет записать hom-тип в таком виде:

type Hom[F[+_]] = [A <: F[Any], B <: F[Any]] =>> A => B

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

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

type HomF[F[_]] = [A, B] =>> F[A] => F[B]

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

Класс типов Category для HomF фиксирован однозначно — для выбранных морфизмов-функций стандартная библиотека Scala предоставляет и тождественный морфизм, и композицию. Получается, единственное, что определяет F-категорию — это конструктор типов F[_]!

Среди всех F-категорий особое значение имеет Id[A] = A, совпадающая с общей категорией типов. Любая категория F[_] является подкатегорией Id[_]. Но в свою очередь, категория F[F[_]] будет целиком лежать внутри F[_], то есть, будет её подкатегорией. Причём, это справедливо для всех категорий, вложенных глубже.

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

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

Другие подкатегории типов

Полезны бывают и другие подкатегории типов, например, основанные на таких hom-типах:

type   Kleisli[F[_]] = [A, B] =>>   A  => F[B]
type CoKleisli[F[_]] = [A, B] =>> F[A] =>   B

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

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

type IntHom  = [A, B] =>> Int 
type Trivial = [A, B] =>> Unit

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

Но тривиальный hom-тип можно переписать следующим образом:

type Trivial = [A, B] =>> Nothing => Nonthing // ≅ Unit

и тогда соответствующую категорию уже можно будет называть подкатегорией типов. Действительно, существует лишь единственный экземпляр identity: Nothing => Nonthing, а значит, этот тип изоморфен Unit и такая категория является тривиальной. С другой стороны, этот hom-тип является функцией, следовательно, мы имеем дело с подкатегорией типов!

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

// комбинатор неподвижной точки двухпараметрического конструктора типов
case class Fix[F[_, _, _[_, _]], A, B](unfix: F[A, B, [X, Y] =>> Fix[F, X, Y]])
// основа "забавной функции", ссылающейся на "себя"
type FancyBase[A, B, Self[_, _]] = A => (Self[A, B], B)
// собственно "забавный" hom-тип
type FancyHom = [A, B] =>> Fix[FancyBase, A, B]

Эта «забавная функция», на самом деле не является настоящей функций. Основанный на ней hom-тип образует самостоятельную категорию, не пересекающуюся с основной категорией типов.

Изоморфизм

Два объекта считаются равными, только если они… равны! Но если это утверждение настолько очевидно, тогда почему же отношениям эквивалентности часто уделяется большое внимание? Дело в том, что в языке математики, как и в любом другом языке используются «псевдонимы», например, чтобы не повторять какое-то сложное понятия каждый раз, а везде использовать лаконичное обозначение этого понятия. И проверяя такие псевдонимы на равенство не всегда бывает очевидно, равнозначны ли скрывающиеся за ними выражения.

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

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

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

type Iso[Hom[_, _]] = [A, B] =>> (
  right: Hom[A, B],
  left : Hom[B, A]
)

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

infix type ≅[A, B] = Iso[Function][A, B]

given iso: (Int, Int) ≅ (Boolean => Int) = ( // Int × Int ≅ Int²
	(pair: (Int, Int)) => (b: Boolean) => if b then pair._2 else pair._1,
	(f: Boolean => Int) => f(false) -> f(true)
)

val guessIdentity = iso.right andThen iso.left // путешествие туда и обратно
guessIdentity((40, 2)) // (40, 2)

В итоге получаем в дополнение к =:= второе соотношение эквивалентности типов ≅ с отличающимся поведением:

summon[(Int, Int) =:= (Boolean => Int)] // не сработает
summon[(Int, Int)  ≅  (Boolean => Int)] // а так - норм

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

Операции с категориями

Дуальная (двойственная) категория

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

Напишем функцию oposite, предоставляющую экземпляр дуальной категории при наличии экземпляра существующей:

type Revert[->[_, _]] = [A, B] =>> B -> A
type Oposite[Cat[_[_, _]]] = [->[_, _]] =>> Cat[Revert[->]]

val oposit: [->[_, _]] => Category[->] ?=> Oposite[Category][->] =
  [->[_, _]] => (cat: Category[->]) ?=> (
    identity = [A] => () => cat.identity[A](),
    compose = [A, B, C] => (f: Revert[->][B, C], g: Revert[->][A, B]) => cat.compose(g, f)
  )

Тривиальный морфизм остался неизменным, но в композиции поменялся порядок морфизмов (f, g) на (g, f).

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

given funcCat: Category[Function] = (
	identity = [A] => () => scala.Predef.identity[A],
	compose  = [A, B, C] => (f: B => C, g: A => B) => f.compose(g)
)

type Coexp = [A, B] =>> B => A

val getAnswer: Coexp[String, Int] = "ответ: " + _
val twice:     Coexp[Int,    Int] = _ * 2
val composed:  Coexp[String, Int] = oposit[Function].compose(twice, getAnswer)

composed(21) // ответ: 42

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

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

Категориальное произведение

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

infix type + = [A, B] =>>  A Either B  
infix type × = [A, B] =>> (A   ,    B)  

Они являются отображением пары типов в тип. Интересный момент заключается в том, что пара типов сама по себе типом не является! Но теория категорий на этом не заканчивается)).

type TypePair[Biconstructor[_, _]] // : ((*, *) => *) => *

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

type CategoryProduct[HomC[_, _]: Category as catC, HomD[_, _]: Category as catD] = (
  identity: [A, B] => () => HomC[A, A] × HomD[B, B],
  compose : [A1, A2, B1, B2, C1, C2] => (HomC[B1, C1] × HomD[B2, C2], HomC[A1, B1] × HomD[A2, B2]) => HomC[A1, C1] × HomD[A2, C2]
)

given categoryProduct: [HomC[_, _]: Category as catC, HomD[_, _] : Category as catD] => CategoryProduct[HomC, HomD] = (
  identity = [C, D] => () => (catC.identity[C](), catD.identity[D]()),
  compose = [A1, A2, B1, B2, C1, C2] => (f: HomC[B1, C1] × HomD[B2, C2], g: HomC[A1, B1] × HomD[A2, B2]) =>
    (catC.compose(f._1, g._1), catD.compose(f._2, g._2))
)

Класс типов CategoryProduct построен по аналогии с Category, описанному выше, только hom-типом везде выступает произведение (кортеж) исходных hom-типов.

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

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

Вот некоторые идеи, которые я надеялся донести в этой части обзора:

• пути вычислений могут пролегать не только через типы, но и в совершенно других категориях;

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

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

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

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