Композитные монады

[Mysterious Light]

Добрый день

Вопрос по программированию, но задаю в этом разделе, потому что в других он смотрится менее уместно.

Зафиксируем категорию типов (д.з.к.). Очевидно, что композиция любых двух функторов — это функтор. А что из себя представляет композиция двух монад?

(Мои рассуждения)

Пусть перед нами две монады $(F_1,\varepsilon_1,\mu_1)$ и $(F_2,\varepsilon_2,\mu_2)$. Построим квадрат

$$ \xymatrix { 1\ar[r]^{\varepsilon_1}\ar[d]_{\varepsilon_2} & F_1 \ar[d]^{F_1\varepsilon_2} \\ F_2\ar[r]_{\varepsilon_1 F_2 } & F_1F_2 }$$

он коммутирует по натуральности $\varepsilon_1$ и поэтому некий аналог единицы (относительно ещё непостроенной операции) $\varepsilon = \varepsilon_1F_2\cdot\varepsilon_2 = \varepsilon_1\cdot F_1\varepsilon_2$ может быть построен.

А вот с умножением большие проблемы. Поскольку речь идёт о программировании, то основные монады — State, Maybe и List. Рассмотрим композицию MaybeState, умножение которой должно иметь тип join :: Maybe (State (Maybe (State a))) -> Maybe (State a), причём по интуиции всё выражение join (Just impureValue) должно возвращать Nothing, если impureValue возвращает Nothing; но это невозможно, поскольку impureValue может менять состояние, а значит возвращаемый тип должен быть по меншей мере State (Maybe a). И действительно, можно описать функцию Maybe (State (Maybe (State a))) -> State (Maybe a) по принципу «внутри монады State разворачиваем капусту из Maybe, пока не дойдём до Nothing и тогда его же и возвращаем или до значения, которое и возвращаем».

С другой стороны, рассмотрим подробнее Maybe a = 1 + a, представленную (не знаю, как правильно это соответствие называется) функцией maybe :: b -> (a -> b) -> Maybe a -> b, т.е. Maybe a ~ forall b. b -> (a -> b) -> b или, по-другому, maybe e f = const e + f
Пусть m — некая монада. Объявим такую функцию:

join a = do
  v <- a
  case v of 
    Nothing -> return Nothing
    Just b  -> b

-- или
join = bind (maybe (return Nothing) id)

где return — $\varepsilon_m$, а bind — это $\mu_m\cdot m$. Введём обозначение N = const Nothing и обратим вниманием, что $N_a : 1\to 1+a$, как и $\operatorname{just}=\varepsilon_{1+a} : a \to 1 + a$, является инъекцией. Перепишем функцию в виде $\mu(a) = \mu_m \circ m \left(\left(\varepsilon_m(1+a) \circ N_a\right) + {\rm id}_{m (1+a)}\right).$
Докажем для примера $\mu\cdot \varepsilon m = {\rm id}$, т.е. $\mu(a)\circ\varepsilon(m(a))$ диаграммой

$$\xymatrix{ m(1+m(1+a)) \ar[d]_{m(\varepsilon_m\circ N+{\rm id})} & 1+m(1+a) \ar[l]_{\varepsilon_m}\ar[d]_{\varepsilon_m\circ N+{\rm id}} && m(1+a) \ar[ll]_{\operatorname{just}} \ar[dll]^{\rm id} \\ m(m(1+a)) \ar[d]_{\mu_m} & m(1+a) \ar[l]^{\varepsilon_m} \ar[dl]^{\rm id} \\ m(1+a) }$$

Верхний левый квадрат естественный для $\varepsilon_m$, правый и нижний треугольники коммутируют по свойству нейтральности единицы отн. умножения для Maybe и m, соответственно.
Полагаю, остальные аксиомы доказываются таким же образом.

(Мои рассуждения 2)

Мне кажется, что для того, чтобы из монад $F_1$ и $F_2$ составить композитную монаду $F_1F_2$, нужно, чтобы было натуральное преобразование $\chi: F_2F_1 \to F_1F_2$. Тогда можно ввести $\mu = \mu_1\mu_2 \cdot F_1\chi F_2$. Однако, нужно бы что-то потребовать, чтобы удовлетворить аксиомам.
Если я правильно рассчитал по подобной прошлой диаграмме схеме, для аксиомы $\mu\cdot\varepsilon F_1F_2 = \operatorname{id}$ нужно потребовать $\varepsilon_2 = \chi \cdot \varepsilon_2F_1.$

Интуитивно, хочется разделить все монады на сильные (IO, State, Writer, Reader) и слабые (Maybe, Either, List), причём первые всегда должны быть где-то снаружи относительно вторых, так сказать, по наличию вышеуказанной функции $\chi$ (например, sequence :: [m a] -> m [a] указывает на слабость списков, а maybe (return Nothing) id :: Maybe (m a) -> m (Maybe a) указывает на слабость Maybe)

А что в литературе говориться по этому вопросу?

[Xaositect]

Да, для монад $M$ и $N$ их композиция $MN$ (как функторов) является монадой тогда и только тогда, когда существует естетсвенное преобразование $NM \Rightarrow MN$, удовлетворяющее определенным аксиомам, которые получаются из аксиом для монад. Это преобразование называется дистрибутивным законом. См. E.Manes, P.Mulry "Monad Compositions I", "Monad Compositions II", и ссылки в них.

Кстати, sequence аксиомам дистрибутивного закона не удовлетворяет, см. https://github.com/manzyuk/blog/blob/ma ... sition.org

[Mysterious Light]

Спасибо, очень интересная работа.

Немного в другом русле задам вопрос:
Как Вы относитесь к трудам Марка Джонса (Mark P. Jones) о манипуляциях с монадами?