Что такое преобразователи монад в Haskell в категорическом выражении?

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

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

Кроме того, глядя на обычные примеры преобразователей монад, в то время как MaybeT m составляет m с Maybe, StateT m не является композицией m с State в любом порядке.

Итак, мой вопрос: что такое преобразователь монад в категориальном языке?


haskell monad-transformers category-theory
person Omar Antolín-Camarena    schedule 28.07.2011    source источник
comment
Они говорят, что преобразователь монад в C - это заостренный эндофунктор (он же премонада) на монаде (C). Я не уверен, что понимаю это определение. Может быть? Тогда поделитесь, пожалуйста;)   -  person n. 1.8e9-where's-my-share m.    schedule 28.07.2011
comment
Эта статья кажется хорошим началом.   -  person hammar    schedule 28.07.2011
comment
@ n.m. Распаковывая заостренный эндофунктор на монаде (C), вы получаете, что преобразователь монад t - это нечто, что (1) для каждой монады m дает вам монаду tm и (2) для каждого морфизма монад m- ›n дает вам другой морфизм монад tm -› tn функционально (т. е. с учетом композиций), а t приходит с (3) для любой монады m, естественным морфизмом монад m - ›tm (т.е. для морфизма монад очевидный квадрат, который вы получаете с вершинами m, n , tm, tn коммутирует). (Эндофунктор на монаде (C) равен (1) и (2), заостренный - (3).)   -  person Omar Antolín-Camarena    schedule 28.07.2011
comment
О, все это объясняется в ссылке на хаммара! (Включая то, что здесь подразумевается под морфизмом монад, термин, который я использовал, но не определял.)   -  person Omar Antolín-Camarena    schedule 28.07.2011
comment
Хорошо, я думаю, что статья hammar, связанная с ответом на мой вопрос: для чего они используются в программировании на Haskell, преобразователям монад нужно только отправлять монады в монады и разрешать дополнительные операции монад. Таким образом, это просто функции из набора монад, даже не эндо функторы на Monad (Hask), хотя на практике все полезные те, за исключением ContT, являются функториальными. Если вы разместите ссылку в качестве ответа, hammar, я буду рад ее принять.   -  person Omar Antolín-Camarena    schedule 28.07.2011
comment
@Omar: Я бы посоветовал вам расширить этот комментарий до ответа на свой вопрос, в этом нет ничего плохого. Просто убедитесь, что он самодостаточный, т.е. добавить ссылку на хаммары = D.   -  person HaskellElephant    schedule 23.11.2011

Ответы (3)


arrow_upward
8
arrow_downward

Трансформаторы монад не очень приятны с математической точки зрения. Однако мы можем получить хорошие (со) продукты из бесплатных монад и, в более общем плане, идеальные монады: см. «Копродукты идеальных монад» Гани и Уусталу: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.2698

person sclv    schedule 28.07.2011
comment
В этой статье вообще не говорится о преобразователях монад (кроме краткого упоминания), поэтому я бы не сказал, что он отвечает на мой вопрос, но он интересен, поэтому спасибо, что указали на него! - person Omar Antolín-Camarena; 28.07.2011
comment
Это действительно позволяет вам получать преобразователи монад формальным, четко определенным и приятным способом, если вы ограничиваете себя вселенной идеальных монад. - person sclv; 29.07.2011
comment
Это верно (и для тех, кто не читал статью, sclv означает, что для любой идеальной монады m вы получаете преобразователь монад, который отправляет монаду n в копроизведение (в категории монад) m и n, и у него есть тоже хорошая конструкция), но я имел в виду то, что, хотя в нем приводятся эти примеры преобразователя монад, в нем не говорится об определении преобразователя монад. - person Omar Antolín-Camarena; 29.07.2011

arrow_upward
3
arrow_downward

Расчет преобразователей монад с помощью теории категорий от Александра Манзюка - это еще одна статья о преобразователях Monad, в которой эта концепция соотносится с важной концепцией присоединения в Теория категорий.
Также, на мой взгляд, в ней используется самая приятная особенность теории категорий, то есть поиск диаграмм, которая натурализует концепцию.
Надеюсь, это поможет.

person awllower    schedule 23.02.2015

arrow_upward
0
arrow_downward

Трансформатор монад - это заостренный эндофунктор в категории монад. В чем проблема?

Вот еще некоторые подробности:

Начнем с некоторой категории, в которой мы рассматриваем те эндофункторы M, которые являются монадами. Все эти монады M образуют категорию, морфизмы которой являются естественными преобразованиями M -> M ', удовлетворяющими законам морфизмов монад.

Трансформатор монад - это заостренный эндофунктор в этой категории монад. Что такое эндофунктор T в этой категории монад? Этот эндофунктор является отображением монады M в монаду T (M) вместе с отображением любого морфизма монад M - ›M 'в морфизм монад T (M) -› T (M').

Эндофунктор T указывается, если существует естественное преобразование из тождественного эндофунктора (Id) в T.

Эндофунктор идентичности - это карта идентичности монад и морфизмов монад. Естественное преобразование Id ~ ›T определяется своими компонентами на всех монадах M. Его компонентой в M является морфизм монад M -> T (M). Кроме того, должен существовать закон естественности (монадическая естественность), который гласит, что для любых монад M и M 'и любого морфизма монад M -> M' диаграмма, состоящая из M, M ', T (M), T ( M ') коммутирует.

Эти данные более или менее совпадают с обычными данными, необходимыми для преобразователя монад. Требуемый морфизм монады M -> T (M) - это подъем чужой монады M в преобразованную монаду.

Конструкция также включает функцию подъема (это действие эндофунктора T на морфизмы монад), которая поднимает морфизмы монад M - ›M 'на T (M) -› T (M').

Если мы рассмотрим образ тождественной монады, T (Id), это должна быть какая-то другая монада. Назовем это базовой монадой преобразователя и обозначим через B. Тогда у нас есть морфизм монады B ~> T (M) для любого M. Это поднятие базовой монады на преобразованную монаду.

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

Распределительные законы применимы только к определенным преобразователям монад. Есть два типа преобразователей, в которых существуют законы распределения: для этих преобразователей составляющая в точке M естественного преобразования Id ~ ›T задается либо M -› B∘M, либо M - ›M∘B. Но у других монад есть преобразователи, которые не являются композициями функторов, и для них нет законов распределения.

Более подробная информация представлена ​​в главе 14 будущей книги «Наука функционального программирования»: https://github.com/winitzki/sofp

person winitzki    schedule 19.05.2021
comment
Это то же самое, что и ответ @hammar 10 лет назад < / а>. - person Omar Antolín-Camarena; 23.05.2021