Категории типов. Часть 6. Расширения Кана

[Dhwtj]

Как и раньше попробую упростить
Практическая часть (конец статьи)

Свободные монады - способ описать программу как данные (AST), а интерпретацию отложить. По сути отделяешь "что делать" от "как делать". Очень DDD-шно звучит, но на практике overhead огромный.

Монады продолжений (Cont) - монада где вычисление принимает "что дальше" как аргумент (callback на стероидах). Даёт контроль над потоком выполнения - можно делать early return, coroutines, backtracking.

Связь: через свободные монады + интерпретатор можно получить эффект продолжений. А Cont монада достаточно мощная чтобы выразить любую другую монаду.

На практике:

• Свободные монады прижились в Haskell (Polysemy, effects systems), немного в Scala (ZIO вдохновлён этим). В остальных языках - академическое упражнение.

• Cont монада - ещё более нишевая, в основном для написания интерпретаторов и компиляторов.

Теоретическая часть (остальное)

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

Структура идёт от общего к частному:

Расширения Кана - самое общее понятие. Маклейн говорил "все понятия теории категорий - это расширения Кана". Из них выводятся:

• Сопряжения (adjunctions) - пары функторов, связанных универсальным свойством. Из них выводятся:

  • (Ко)пределы - обобщение произведений, сумм, уравнителей

  • Представления Йонеды - любой объект полностью определяется морфизмами в/из него

Коплотность - связь между функтором и его "приближением" через расширения Кана. Отсюда выводится:

• Монада коплотности - каноническая монада, порождённая функтором

• Монада передачи продолжений (CPS) - частный случай монады коплотности

• Свободная монада - выражается через левое расширение Кана, потом оптимизируется

То есть текст показывает, что Cont монада и Free монада - это конкретные инстансы одной и той же категорной машинерии (расширений Кана). Они не просто "похожи", а буквально выводятся из одного корня.

Уровень - продвинутая теория категорий.

[Underskyer1]

Спасибо, но не совсем так.

Принципиально большого "overhead" в технике свободных монад нет. По сути, не больше чем в традиционном DDD, когда, например, абстракции описываются в одном модуле, а реализации - в другом. Наибольшая проблема - в излишней "двухэтапности" выполнения накапливаемой программы-как-данные. С этим пытается бороться техника Tagless Final, но вот там сложнее избавиться от "лишнего кода".

В Scala есть специальная техника программирования, основанная на свободных монадах. И есть продуктовый код, написанный в этом стиле. Свободные монады "вдохновили" скалистов прежде всего на cats.data.Eval, cats.effect.IO и только позднее уже на zio.ZIO. А монада продолжения явно используется не часто как раз потому, что её преимущества зачастую уже реализованы в компиляторах и библиотеках.

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

Проблема большинства публикаций на тему монад, их композиции, свободных монад, продолжений и т.п. - это необоснованное неконструктивное определение абстракций, которые "просто работают" ("пользуйтесь, не задавая вопросов"). У программистов часто возникает впечатление типа "ах, ещё одна хрень, мне и без неё нормально с тем, к чему я уже привык". А пытливые умы пытаются выбрать из всей этой каши детали для "наилучшей" техники программирования.

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

[Dhwtj]

Я так и подумал, что вы про Scala

Потому что в других языках топ-20 этого нет, а библиотеки выглядят по уродски не идиоматично