Всегда ли композиция произвольной монады с проходимым монадой?

Если у меня есть две монады m а также n, а также n проходимо, обязательно ли у меня составной m-над-n монада?

Более формально вот что я имею в виду:

import Control.Monad
import Data.Functor.Compose

prebind :: (Monad m, Monad n) =>
         m (n a) -> (a -> m (n b)) -> m (n (m (n b)))
mnx `prebind` f = do nx <- mnx
                     return $ do x <- nx
                                 return $ f x

instance (Monad m, Monad n, Traversable n) => Monad (Compose m n) where
  return = Compose . return . return
  Compose mnmnx >>= f = Compose $ do nmnx <- mnmnx `prebind` (getCompose . f)
                                     nnx  <- sequence nmnx
                                     return $ join nnx

Естественно, эта проверка типов, и я считаю, работает для нескольких случаев, которые я проверял (Reader over List, State over List) - например, составленная "монада" удовлетворяет законам монады - но я не уверен, что это это общий рецепт для наложения любой монады на проходимую.

Источник

2 ответа

Решение

Нет, это не всегда монада. Вам нужны дополнительные условия совместимости, относящиеся к монадным операциям двух монад и закону распределения. sequence :: n (m a) -> m (n a), как описано, например, в Википедии.

Ваш предыдущий вопрос приводит пример, в котором условия совместимости не выполняются, а именно

S = m = [], с единицей X -> SX, отправляющей x в [x];

T = n = (->) Boolили, что то же самое, TX = X × X, причем единица X -> TX отправляет x в (x,x).

Правая нижняя диаграмма на странице Википедии не коммутирует, так как композиция S -> TS -> ST отправляет xs :: [a] в (xs,xs) а затем к декартову произведению всех пар, взятых из xs; в то время как правая карта S -> ST отправляет xs на "диагональ", состоящую только из пар (x,x) за x в xs, Это та же проблема, из-за которой предложенная монада не удовлетворяла одному из законов юнитов

Источник

Несколько дополнительных замечаний, чтобы сделать связь между общим ответом Рейда Бартона и вашим конкретным вопросом более явной.

В этом случае это действительно окупается Monad пример с точки зрения join:

join' ::  m (n (m (n b))) -> m (n b)
join' = fmap join . join . fmap sequence

Повторно вводя compose/getCompose в соответствующих местах и ​​используя m >>= f = join (fmap f m), вы можете проверить, что это действительно эквивалентно вашему определению (обратите внимание, что ваш prebind составляет fmap f в этом уравнении).

Это определение позволяет проверить законы с помощью диаграмм1. Вот один для join . return = id т.е. (fmap join . join . fmap sequence) . (return . return) = id:

3210 MT ID MT ID MT ID MT
     ---->      ---->     ---->
 rT2 |   |  rT1 |   | rT1 |   | id
 rM3 V   V  rM3 V   V     V   V
     ---->      ---->     ---->
MTMT  sM2  MMTT  jM2  MTT  jT0  MT

Общий прямоугольник - это закон монады:

 M id M
    ---->     
rM1 | | Я бы 
    ВВ ---->     
 MM  jM0  M

Игнорируя части, которые обязательно одинаковы в обоих направлениях через квадраты, мы видим, что два самых правых квадрата равносильны одному и тому же закону. (Конечно, немного глупо называть эти "квадраты" и "прямоугольники", учитывая все id у них есть стороны, но это лучше подходит моим ограниченным художественным навыкам ASCII.) Первый квадрат, тем не менее, составляет sequence . return = fmap return, которая является правой нижней диаграммой на странице Википедии, упоминает Рейд Бартон...

 M id M
    ---->     
rT1 | | RT0 
    ВВ ---->     
 ТМ СМ1 МТ

... и это не дано, что верно, как показывает ответ Рейда Бартона.

Если мы применим ту же стратегию к join . fmap return = id закон, правая верхняя диаграмма, sequence . fmap return = return, показывает, что, однако, это не проблема сама по себе, поскольку это просто (непосредственное следствие) закон идентичности Traversable, Наконец, сделать то же самое с join . fmap join = join . join закон делает две другие диаграммы - sequence . fmap join = join . fmap sequence . sequence а также sequence . join = fmap join . sequence . fmap sequence - весна вперед.

Примечания:

  1. Легенда для стенографии: r является return, s является sequence а также j является join, Буквы и цифры в верхнем регистре после сокращений функций устраняют неоднозначность для задействованной монады, и позиция ее введенного или измененного слоя заканчивается на - в случае s, что относится к тому, что изначально является внутренним слоем, так как в этом случае мы знаем, что внешний слой всегда T, Слои нумеруются снизу вверх, начиная с нуля. Композиция указывается путем написания сокращенной записи для второй функции под первой.
Источник
Другие вопросы по тегам