Обзор, посвящённый применению элементов теории категорий в программировании, завершён. Настало время подвести его итоги.

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

8.1. Вертикальная композиция эффектов

8.2. Горизонтальная композиция эффектов

Итоги

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

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

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

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

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

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

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

Также выясняется, что любая монада может быть разложена на пары сопряжённых функторов, проходящих через промежуточные категории. Оказывается, все такие сопряжения монады образуют собственную категорию, в которой особенное значение имеют начальный и терминальный объекты. Им и посвящена следующая промежуточная часть обзора. Начальный объект — это сопряжение Клейсли, которое описывает монаду как интерфейс для композиции стрелок вида A => F[B]. С другой стороны стоит терминальное сопряжение Эйленберга‑Мура, наделяющее монаду смыслом лишь в том случае, когда для неё предоставлен механизм «распаковки» F[A] => A.

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

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

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

И только теперь, под конец обзора появилась возможность детально разобрать проблему композиции монад. Тема оказалось объёмной, поэтому пришлось разбить её на две публикации.

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

Вторая публикация посвящена горизонтальной композиции алгебраических эффектов. Она уже мало отношения имеет к теории категорий, но для полноты картины без неё не обойтись. Горизонтальная композиция обычно осуществляется с использованием свободных монад, техники Tagless Final, а также она является ключевой для императивного стиля (direct style). Так или иначе, но всё сводится к предоставлению (экспоненциалу) набора (произведения) обработчиков для суммы эффектов. Различные реализации горизонтальной композиции имеют свои отличия, но самыми концептуальными из них являются лишь синтаксические.

Теория категорий даёт программированию следующее:

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

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

Спасибо за внимание!

Категории типов. Итоги