Свежий пейпер "Evolution of Stacks and Moduli" (современные методы построения пространств модулей) Вашингтонского универа, где не рассказывается, а мы уже сами, по заветам Гротендика, выводим в наши интересы, что тамошний "стек" -- это "тип с контекстом выполнения", где равенство типов заменено эквивалентностью морфизмов. То есть это прямая аналогия между 2-категориями/стеками (пруф) и типизированными эффектами!

В завтипчиках мы можем иметь тип изоморфизма, но в стеке мы проверяем не равенство объектов, а выясняем, как именно они изоморфны, и как в нём склеивать объекты.

Монады -- это частный случай стеков (категория Клейсли для монады), и мы можем теперь композировать эффекты не только последовательно, но и параллельно, с синхронизацией по изоморфизмам!

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

Ну и? Ну это всё например хаскелевские темки Parameterized monads и Graded monads, которые можно поразвивать.

А для моего обучающего агента я выжал отсюда чек-лист "корректен ли код с точки зрения теории категорий". Например, что ты будешь делать, если у объекта появится нетривиальный автоморфизм?:)