2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

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

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

Обязательно просмотрите тему Правила данного раздела, иначе Ваша тема может быть удалена или перемещена в Карантин, а Вы так и не узнаете, почему.



Начать новую тему Ответить на тему
 
 Композитные монады
Сообщение14.12.2014, 20:12 
Аватара пользователя


29/05/11
227
Красноармейск, Донецкая обл.
Добрый день

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

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

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

Пусть перед нами две монады $(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)

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

 Профиль  
                  
 
 Re: Композитные монады
Сообщение14.12.2014, 23:37 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Да, для монад $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

 Профиль  
                  
 
 Re: Композитные монады
Сообщение01.01.2015, 23:44 
Аватара пользователя


29/05/11
227
Красноармейск, Донецкая обл.
Спасибо, очень интересная работа.

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 3 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group