Why does mutual yielding make ArrowApply and Monads equivalent, unlike Arrow and Applicative?

Question

Here's the SO post I'm going to refer to. Also, I'm going to use the same snippets as the OP in that question in order not to separate the materials.

It is widely known that an ArrowApply instance yields a Monad and vice versa:

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))

And until I've stumbled upon the post referenced above, I felt that this snippet was a plausible proof for the equivalence of ArrowApply and Monad classes. Yet, having the knowledge that Arrow and Applicative are not, in fact, equivalent and the following snippet made me curious about the full proof of equivalency of Monad and 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

Thus if you round trip through applicative you lose some features.

It is obvious with the examples written down, yet I fail to grasp how is "round-tripping" through Monad preserves all the ArrowApply features since initially we had an arrow which depends on some input (a b c) but in the end, we end up with an arrow forced into a wrapper which has unit type as its input type (ArrowMonad (a () b)).

It is obvious that I'm doing something awfully wrong here, yet I cannot understand what exactly.

What is the full proof that ArrowApply and Monad are equivalent?

What do the examples of inequivalence of Arrow and Applicative account for? Does one generalise another?

What is the interpretation of that whole situation in arrow calculus and category theory?

I would appreciate both full explanations and tips which could help one draw up a plausible piece of proof themself.

leftaroundabout leftaroundabout · Accepted Answer · 2020-01-24T13:19:22

since initially we had an arrow which depends on some input (a b c) but in the end, we end up with an arrow forced into a wrapper which has unit type as its input type (ArrowMonad (a () b))

I guess this is the central point of confusion, and indeed it is confusing. I like to think of arrows as mostly morphisms in a cartesian monoidal category, where you wouldn't get this, but already the Arrow class is actually more restrictive than that thanks to arr – which gives you a functor from Hask into the category. But, somewhat surprisingly, that also entails that you get a mapping in the other direction: any arrow can be replaced with a function which yields merely an arrow of trivial domain. Concretely,

arrAsFunction :: Arrow k => k x y -> (x -> k () y)
arrAsFunction φ x = φ <<< arr (const x)

Ok that alone wouldn't be too groundbraking – maybe we've just discarded some information here? – but with ArrowApply this is actually an isomorphism: you can get back the original arrow by way of

retrieveArrowFromFunction :: ∀ k x y .
          ArrowApply k => (x -> k () y) -> k x y
retrieveArrowFromFunction f = arr f' >>> app
 where f' :: x -> (k () y, ())
       f' x = (f x, ())

...which is exactly what's used in the Monad (ArrowMonad a) instance.

So the upshot is: arr, by requiring that you can embed any Haskell function in the category, enforces that the category basically boils down to functions with some wrapper around the result, IOW something like Kleisli arrows.

Check out some other category-theory hierarchies to see that this is not a fundamental feature of cartesian monoidal categories, but really an artifact of the Hask → k functor. E.g. in constrained-categories I've mirrored the standard classes closely, with PreArrow as the class of cartesian monoidal categories, but deliberately kept arr out of it and didn't make it specific to Hask, because that dumbs down the capabilities of the category too much and causes it to be almost-equivalent to Hask-Kleisli.

Why does mutual yielding make ArrowApply and Monads equivalent, unlike Arrow and Applicative?

1 Answers