Что является примером Monad, который является Альтернативой, но не MonadPlus?

Question

В своем ответе на вопрос "Различие между классами типов MonadPlus , Alternative , а также Monoid ? ", Говорит Эдвард Кметт

Более того, даже если Applicative был суперклассом Monad Вы бы нуждались в MonadPlus класс в любом случае, потому что подчиняясь

empty <*> m = empty

не достаточно строго, чтобы доказать это

empty >>= f = empty

Так утверждая, что что-то MonadPlus сильнее, чем утверждать, что это Alternative,

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

---

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

1. Правильное распределение (из <*> ): (f <|> g) <*> a = (f <*> a) <|> (g <*> a)
2. Правильное поглощение (для <*> ): empty <*> a = empty
3. Левая дистрибутивность (из fmap ): f <$> (a <|> b) = (f <$> a) <|> (f <$> b)
4. Левое поглощение (для fmap ): f <$> empty = empty

Я также с радостью согласился бы получить более полезный набор Alternative законы.

² Я знаю, что есть некоторая двусмысленность в том, что MonadPlus законы есть; Я доволен ответом, в котором используется левый дистрибутив или левый улов, хотя я бы слабо предпочел первый.

Answer 1

Подсказка к вашему ответу есть в HaskellWiki о MonadPlus, на который вы ссылаетесь:

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

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

Maybe альтернатива

1. Правильное распределение (из <*> ): (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 <*>

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

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

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

1. Левая дистрибутивность (из 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 <$>

1. Левое поглощение (для 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

здесь я использовал связывание (>>=) вырвать неудачу (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)