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

Question

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

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

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 

Естественно, этот тип-чеки, и я считаю, работает в течение нескольких случаев, которые я проверил (Читатель более Список, государство через список) - как и в, сочиненная «монада» удовлетворяет законам монады, но я не уверен, что это общий рецепт для разбиения любой монады на обходной.

Answer 1

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

Your previous question приведен пример, в котором условие совместимости не выполняется, а именно

S = m = [], с блоком X -> SX посылая й в [х];

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

Answer 2

Несколько дополнительных замечаний, чтобы сделать связь между Reid Barton's general answer и конкретным конкретным вопросом более явным.

В этом случае, действительно окупается отработать свой 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 в этом уравнении).

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

 

    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 

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

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

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

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

---

Сноски:

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