Какой пример Монады, которая является альтернативой, но не MonadPlus?

Ясно, что любой прикладной функтор, который не является монадой, автоматически является примером Alternative, который не является MonadPlus, но ответ Эдварда Кемца предполагает, что существует монада, которая является Alternative, но не является MonadPlus: его empty и <|> будут удовлетворять законам Alternative, ¹ но не законы MonadPlus. ² Я не могу придумать пример этого сам; кто-нибудь знает об одном?

¹ Я не смог найти каноническую ссылку для набора законов Alternative, но я излагаю, что я считаю, что они примерно на полпути через мой ответ на вопрос "Confused значением класса типа Alternative и его отношением к другим классам классов" (поиск фразы "правая дистрибутивность" ). Четыре закона, которые, как я полагаю, должны быть выполнены, заключаются в следующем:

Id также счастливо признается, что ему дается более полезный набор законов Alternative.

Ответы

Ответ 1

Ключ к вашему ответу находится в HaskellWiki о MonadPlus, который вы связали с:

Какие правила? Мартин и Гиббонс выбирают Monoid, Left Zero и Left Distribution. Это делает [] MonadPlus, но не Maybe или IO.

Итак, в соответствии с вашим предпочтительным выбором Maybe не является MonadPlus (хотя есть экземпляр, он не удовлетворяет левому распределению). Пусть оно удовлетворяет альтернативе.

`Maybe` является альтернативой

Правильная дистрибутивность (<*>): (f <|> g) <*> a = (f <*> a) <|> (g <*> a)

Случай 1: f=Nothing:

(Nothing <|> g) <*> a =                    (g) <*> a  -- left identity <|>
                      = Nothing         <|> (g <*> a) -- left identity <|>
                      = (Nothing <*> a) <|> (g <*> a) -- left failure <*>

Случай 2: a=Nothing:

(f <|> g) <*> Nothing = Nothing                             -- right failure <*>
                      = Nothing <|> Nothing                 -- left identity <|>
                      = (f <*> Nothing) <|> (g <*> Nothing) -- right failure <*>

Случай 3: f=Just h, a = Just x

(Just h <|> g) <*> Just x = Just h <*> Just x                      -- left bias <|>
                          = Just (h x)                             -- success <*>
                          = Just (h x) <|> (g <*> Just x)          -- left bias <|>
                          = (Just h <*> Just x) <|> (g <*> Just x) -- success <*>

Правильное поглощение (для <*>): empty <*> a = empty

Это легко, потому что

Nothing <*> a = Nothing    -- left failure <*>

Левая дистрибутивность (fmap): f <$> (a <|> b) = (f <$> a) <|> (f <$> b)

Случай 1: a = Nothing

f <$> (Nothing <|> b) = f <$> b                        -- left identity <|>
                 = Nothing <|> (f <$> b)          -- left identity <|>
                 = (f <$> Nothing) <|> (f <$> b)  -- failure <$>

Случай 2: a = Just x

f <$> (Just x <|> b) = f <$> Just x                 -- left bias <|>
                     = Just (f x)                   -- success <$>
                     = Just (f x) <|> (f <$> b)     -- left bias <|>
                     = (f <$> Just x) <|> (f <$> b) -- success <$>

Левое поглощение (для fmap): f <$> empty = empty

Еще один простой:

f <$> Nothing = Nothing   -- failure <$>

`Maybe` не является MonadPlus

Докажем утверждение, что Maybe не является MonadPlus: нам нужно показать, что mplus a b >>= k = mplus (a >>= k) (b >>= k) не всегда выполняется. Трюк, как всегда, использовать некоторую привязку, чтобы скрывать самые разные значения:

a = Just False
b = Just True

k True = Just "Made it!"
k False = Nothing

Теперь

mplus (Just False) (Just True) >>= k = Just False >>= k
                                     = k False
                                     = Nothing

здесь я использовал bind (>>=), чтобы вырвать сбой (Nothing) из челюстей победы, потому что Just False выглядел как успех.

mplus (Just False >>= k) (Just True >>= k) = mplus (k False) (k True)
                                           = mplus Nothing (Just "Made it!")
                                           = Just "Made it!"

Здесь неудача (k False) была рассчитана раньше, поэтому она проигнорировалась и мы "Made it!".

Итак, mplus a b >>= k = Nothing, но mplus (a >>= k) (b >>= k) = Just "Made it!".

Вы можете посмотреть на это, как я, используя >>=, чтобы сломать левое смещение mplus для Maybe.

Действительность моих доказательств:

На всякий случай, если бы вы чувствовали, что я не сделал достаточно утомительного вывода, я докажу, что я использовал:

Во-первых,

Nothing <|> c = c      -- left identity <|>
Just d <|> c = Just d  -- left bias <|>

которые исходят из объявления экземпляра

instance Alternative Maybe where
    empty = Nothing
    Nothing <|> r = r
    l       <|> _ = l

Во-вторых

f <$> Nothing = Nothing    -- failure <$>
f <$> Just x = Just (f x)  -- success <$>

который только что пришел из (<$>) = fmap и

instance  Functor Maybe  where
    fmap _ Nothing       = Nothing
    fmap f (Just a)      = Just (f a)

В-третьих, остальные три выполняют немного больше работы:

Nothing <*> c = Nothing        -- left failure <*>
c <*> Nothing = Nothing        -- right failure <*>
Just f <*> Just x = Just (f x) -- success <*>

Что происходит из определений

instance Applicative Maybe where
    pure = return
    (<*>) = ap

ap :: (Monad m) => m (a -> b) -> m a -> m b
ap =  liftM2 id

liftM2  :: (Monad m) => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 f m1 m2          = do { x1 <- m1; x2 <- m2; return (f x1 x2) }

instance  Monad Maybe  where
    (Just x) >>= k      = k x
    Nothing  >>= _      = Nothing
    return              = Just

так

mf <*> mx = ap mf mx
          = liftM2 id mf mx
          = do { f <- mf; x <- mx; return (id f x) }
          = do { f <- mf; x <- mx; return (f x) }
          = do { f <- mf; x <- mx; Just (f x) }
          = mf >>= \f ->
            mx >>= \x ->
            Just (f x)

поэтому, если mf или mx ничего, результат также Nothing, тогда как если mf = Just f и mx = Just x, результат Just (f x)