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

Если у меня есть две монады m и n, а n - проходящая, обязательно ли у меня есть композитная m -over- 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) - как и в, составленная "монада" удовлетворяет законам монады, но я unsure, если это общий рецепт для разбиения любой монады на проходящую через нее.

Ответы

Ответ 1

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

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

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. Это та же самая проблема, из-за которой ваша предлагаемая монада не удовлетворяет одному из законов единицы.

Ответ 2

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

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

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

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

Это определение позволяет удобно проверять законы с диаграммами 1. Вот один для join. return = id join. return = id ie (fmap join. join. fmap sequence). (return. 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 |   | id 
    V   V  
    ---->     
 MM  jM0  M

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

 M   id   M
    ---->     
rT1 |   | rT0 
    V   V  
    ---->     
 TM  sM1  MT

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

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

Примечания:

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