Hier ist der SO-Beitrag, auf den ich mich beziehen werde .Außerdem werde ich in dieser Frage dieselben Schnipsel wie das OP verwenden, um die Materialien nicht zu trennen .
Es ist allgemein bekannt, dass eine ArrowApply
Instanz eine Monade ergibt und umgekehrt:
newtype ArrowMonad a b = ArrowMonad (a () b)
instance Arrow a => Functor (ArrowMonad a) where
fmap f (ArrowMonad m) = ArrowMonad $ m >>> arr f
instance Arrow a => Applicative (ArrowMonad a) where
pure x = ArrowMonad (arr (const x))
ArrowMonad f <*> ArrowMonad x = ArrowMonad (f &&& x >>> arr (uncurry id))
instance ArrowApply a => Monad (ArrowMonad a) where
ArrowMonad m >>= f = ArrowMonad $
m >>> arr (\x -> let ArrowMonad h = f x in (h, ())) >>> app
newtype Kleisli m a b = Kleisli { runKleisli :: a -> m b }
instance Monad m => Category (Kleisli m) where
id = Kleisli return
(Kleisli f) . (Kleisli g) = Kleisli (\b -> g b >>= f)
instance Monad m => Arrow (Kleisli m) where
arr f = Kleisli (return . f)
first (Kleisli f) = Kleisli (\ ~(b,d) -> f b >>= \c -> return (c,d))
second (Kleisli f) = Kleisli (\ ~(d,b) -> f b >>= \c -> return (d,c))
Und bis ich auf den oben genannten Beitrag gestoßen bin , hatte ich das Gefühl, dass dieser Ausschnitt ein plausibler Beweis für die Gleichwertigkeit ArrowApply
und Monad
Klassen ist. Das Wissen, dass Arrow und Applicative tatsächlich nicht gleichwertig sind, und der folgende Ausschnitt haben mich neugierig gemacht auf den vollständigen Beweis der Gleichwertigkeit von Monad
und ArrowApply
:
newtype Arrplicative arr o a = Arrplicative{ runArrplicative :: arr o a }
instance (Arrow arr) => Functor (Arrplicative arr o) where
fmap f = Arrplicative . (arr f .) . runArrplicative
instance (Arrow arr) => Applicative (Arrplicative arr o) where
pure = Arrplicative . arr . const
Arrplicative af <*> Arrplicative ax = Arrplicative $
arr (uncurry ($)) . (af &&& ax)
newtype Applicarrow f a b = Applicarrow{ runApplicarrow :: f (a -> b) }
instance (Applicative f) => Category (Applicarrow f) where
id = Applicarrow $ pure id
Applicarrow g . Applicarrow f = Applicarrow $ (.) <$> g <*> f
instance (Applicative f) => Arrow (Applicarrow f) where
arr = Applicarrow . pure
first (Applicarrow f) = Applicarrow $ first <$> f
> Wenn Sie also eine Rundreise durch die Anwendung machen, verlieren Sie einige Funktionen.
Es ist offensichtlich, ob die Beispiele bereitgestellt werden, aber ich verstehe nicht, wie beim "Roundtripping" durch Monad alle ArrowApply-Funktionen erhalten bleiben, da wir anfangs einen Pfeil hatten, der von einer Eingabe abhängt ( a b c
), aber am Ende haben wir Ein Pfeil, der in einen Wrapper gezwungen wird, dessen Eingabetyp der Einheitentyp ist ( ArrowMonad (a () b)
).
Es ist offensichtlich, dass ich hier etwas furchtbar Falsches mache, aber ich kann nicht genau verstehen, was.
Was ist der vollständige Beweis dafür, dass ArrowApply
undMonad
sind gleichwertig?
Was bedeuten die Beispiele für die Ungleichwertigkeit von Arrow
undApplicative
erklären erklären ? Verallgemeinert einer den anderen?
Wie ist die Interpretation dieser ganzen Situation in der Pfeilrechnung und der Kategorietheorie?
Ich würde mich sowohl über vollständige Erklärungen als auch über Tipps freuen, die dazu beitragen könnten, selbst einen plausiblen Beweis zu erstellen.
quelle