Welche Beziehungen bestehen zwischen Alternative, MonadPlus (LeftCatch) und MonadPlus (LeftDistributive)?

12

Follow up Was ist ein Beispiel für eine Monade, die eine Alternative ist, aber keine MonadPlus? :

Angenommen, ist eine Monade. Was sind die Beziehungen betweem ein Wesen Alternative , eine MonadPlusCatch und MonadPlusDistr ? mmFür jedes der sechs möglichen Paare hätte ich gerne entweder einen Beweis, dass eines ein anderes impliziert, oder ein Gegenbeispiel, dass dies nicht der Fall ist.

(Ich benutze

  • MonadPlusCatch zur Unterscheidung eines MonadPlus , der die Left-Catch- Regel erfüllt :

    mplus (return a) b = return a
    
  • MonadPlusDistr eine unterscheiden MonadPlus dass erfüllt hierbei Linksverteilungsregel:

    mplus a b >>= k = mplus (a >>= k) (b >>= k)
    

siehe MonadPlus auf HaskellWiki .)


Mein aktuelles Wissen und meine Intuition sind folgende:

  1. MonadPlusDist Alternative - wahrscheinlich wahr - es scheint einfach zu sein, ich glaube, ich habe eine Skizze eines Beweises, ich werde es überprüfen und wenn es korrekt ist, werde ich es posten. AndrewC hat diesen Teil beantwortet.
  2. Maybe
  3. MaybeT (Either e)MaybeT m'

    ((pure x) <|> g) <*> a =    -- LeftCatch
        (pure x) <*> a
    -- which in general cannot be equal to
    ((pure x) <*> a) <|> (g <*> a)
    

    Ich werde nochmal nachsehen und posten. (Interessanterweise für nur Maybees ist beweisbar, weil wir analysieren können , wenn aist Just somethingoder Nothing- vgl . Die vorgenannte AndrewC Antwort)

  4. [][]
  5. []
  6. Maybe
Petr Pudlák
quelle

Antworten:

8

(Weil, wie Petr Pudlák betonte, []ein Gegenbeispiel ist - es erfüllt nicht MonadPlusCatch, sondern MonadPlusDist , daher Applicative )

Angenommen: MonadPlusDist-Gesetze

-- (mplus,mzero) is a monoid
mzero >>= k = mzero`                             -- left identity >>=
(a `mplus` b) >>= k  =  (a >>=k) `mplus` (b>>=k) -- left dist mplus

Um zu beweisen: Alternative Gesetze

-- ((<|>),empty) is a monoid
(f <|> g) <*> a = (f <*> a) <|> (g <*> a) -- right dist <*>
empty <*> a = empty                       -- left identity <*>
f <$> (a <|> b) = (f <$> a) <|> (f <$> b) -- left dist <$>
f <$> empty = empty                       -- empty fmap

<*>Expansions-Lemma
Angenommen, wir verwenden die Standardableitung eines Applikativs aus einer Monade, nämlich (<*>) = apund pure = return. Dann

mf <*> mx = mf >>= \f -> mx >>= \x -> return (f x)

da

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

<$>Erweiterungs-Lemma
Angenommen, wir verwenden die Standardableitung eines Funktors von einer Monade, nämlich (<$>) = liftM. Dann

f <$> mx = mx >>= return . f

da

f <$> mx = liftM f mx                    -- premise
         = do { x <- mx; return (f x) }  -- def(liftM)
         = mx >>= \x -> return (f x)     -- desugaring
         = mx >>= \x -> (return.f) x     -- def((.))
         = mx >>= return.f               -- eta-reduction 

Beweis

Angenommen, ( <+>, m0) erfüllen die MonadPlus-Gesetze. Trivialerweise ist es dann ein Monoid.

Right Dist <*>

Ich werde es beweisen

(mf <+> mg) <*> ma = (mf <*> ma) <+> (mg <*> ma) -- right dist <*>

weil es einfacher für die Notation ist.

(mf <+> mg) <*> ma = (mf <+> mg) >>= \forg -> mx >>= \x -> return (forg x) -- <*> expansion
                   =     (mf >>= \f_g -> mx >>= \x -> return (f_g x))
                     <+> (mg >>= \f_g -> mx >>= \x -> return (f_g x))      -- left dist mplus
                   = (mf <*> mx) <+> (mg <*> mx)                           -- <*> expansion

Linke Identität <*>

mzero <*> mx = mzero >>= \f -> mx >>= \x -> return (f x) -- <*> expansion
             = mzero                                     -- left identity >>=

nach Bedarf.

Left Dist <$>

f <$> (a <|> b) = (f <$> a) <|> (f <$> b) -- left dist <$>

f <$> (a <+> b) = (a <+> b) >>= return . f              -- <$> expansion
                = (a >>= return.f) <+> (b >>= return.f) -- left dist mplus
                = (f <$> a) <+> (f <$> b)               -- <$> expansion

empty fmap

f <$> mzero = mzero >>= return.f   -- <$> expansion
            = mzero                -- left identity >>=

nach Bedarf

AndrewC
quelle
1
Groß. Ich vermute sogar, dass die Linksgesetze durch die Rechtsgesetze für jeden Antragsteller impliziert werden , aber ich habe bisher keinen Beweis. Die Intuition ist, dass f <$>es keine idiomatische Handlung gibt, es ist rein, so dass es möglich sein könnte, irgendwie "die Seiten zu wechseln".
Petr Pudlák
@PetrPudlák Aktualisiert - beendete den Beweis und fügte deine Korollorie über [].
AndrewC
@ PetrPudlák Meinen Sie, wir sollten einen Beweis hinzufügen, []der MonadPlusCatch erfüllt ? Im Moment ist es nur eine Behauptung im HaskellWiki. >>= kwird explizit mitfoldr ((++).k)
AndrewC 31.10.12
Ich nehme an, Sie meinen MonadPlusDist , nicht wahr ? Ich denke wir könnten, dies würde den Beweis der Folgerung vervollständigen.
Petr Pudlák
@PetrPudlák Oh ja tut mir leid. Wird besorgt.
AndrewC
6

In der Tat ist es MaybeT Either:

{-# LANGUAGE FlexibleInstances #-}
import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Maybe

instance (Show a, Show b) => Show (MaybeT (Either b) a) where
    showsPrec _ (MaybeT x) = shows x

main = print $
    let
        x = id :: Int -> Int
        g = MaybeT (Left "something")
        a = MaybeT (Right Nothing)
    -- print the left/right side of the left distribution law of Applicative:
    in ( ((return x) `mplus` g) `ap` a
       , ((return x) `ap` a) `mplus` (g `ap` a)
       )

Die Ausgabe ist

(Right Nothing, Left "something")

was bedeutet, dass das MaybeT EitherLinkverteilungsgesetz von Applicative.


Der Grund ist, dass

(return x `mplus` g) `ap` a

ignoriert g(aufgrund von LeftCatch ) und wertet nur zu aus

return x `ap` a

Dies unterscheidet sich jedoch von dem, was die andere Seite bewertet:

g `ap` a
Petr Pudlák
quelle