¿Por qué el rendimiento mutuo hace que ArrowApply y Monads sean equivalentes, a diferencia de Arrow y Applicative?

Aquí está la publicación SO a la que me referiré . Además, voy a usar los mismos fragmentos que el OP en esa pregunta para no separar los materiales .

Es ampliamente conocido que una ArrowApplyinstancia produce una mónada y viceversa:

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

Y hasta que me topé con la publicación mencionada anteriormente, sentí que este fragmento era una prueba plausible de la equivalencia de ArrowApplyy las Monadclases. Sin embargo, tener el conocimiento de que Arrow y Applicative no son, de hecho, equivalentes y el siguiente fragmento me hizo sentir curiosidad acerca de la prueba completa de equivalencia de Monady 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

> Por lo tanto, si realiza un viaje de ida y vuelta a través de aplicativo, pierde algunas características. Es obvio si se proporcionan los ejemplos, pero no entiendo cómo es que el "viaje de ida y vuelta" a través de Monad conserva todas las características de ArrowApply, ya que inicialmente teníamos una flecha que depende de alguna entrada ( a b c) pero al final, terminamos con una flecha forzada en un contenedor que tiene el tipo de unidad como su tipo de entrada ( ArrowMonad (a () b)).

Es obvio que estoy haciendo algo terriblemente mal aquí, pero no puedo entender exactamente qué.

¿Cuál es la prueba completa de que ArrowApplyy Monadson equivalentes?

¿Qué explican los ejemplos de desigualdad de Arrowy Applicative? ¿Uno generaliza a otro?

¿Cuál es la interpretación de toda esa situación en el cálculo de flechas y la teoría de categorías?

Agradecería tanto las explicaciones completas como los consejos que podrían ayudarnos a elaborar una prueba plausible.

dado que inicialmente teníamos una flecha que depende de alguna entrada ( a b c) pero al final, terminamos con una flecha forzada en un contenedor que tiene el tipo de unidad como su tipo de entrada ( ArrowMonad (a () b))

Supongo que este es el punto central de confusión, y de hecho es confuso. Me gusta pensar que las flechas son en su mayoría morfismos en una categoría monoidal cartesiana, donde no obtendrías esto, pero la Arrowclase ya es más restrictiva que eso arr, lo que te da un functor de Hask en la categoría. Pero, algo sorprendente, eso también implica que se obtiene un mapeo en la otra dirección: cualquier flecha se puede reemplazar con una función que produce simplemente una flecha de dominio trivial. Concretamente

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

Ok, eso solo no sería demasiado innovador, ¿tal vez acabamos de descartar alguna información aquí? - pero con ArrowApplyesto en realidad es un isomorfismo : puede recuperar la flecha original a través de

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

... que es exactamente lo que se usa en la Monad (ArrowMonad a)instancia.

Entonces, el resultado es que arr, al exigir que pueda incrustar cualquier función de Haskell en la categoría, impone que la categoría básicamente se reduzca a funciones con algún envoltorio alrededor del resultado , IOW algo como flechas de Kleisli.

Echa un vistazo a algunas otras jerarquías de teoría de categorías para ver que esta no es una característica fundamental de las categorías monoidales cartesianas, sino que realmente es un artefacto del funk Hask → k . Por ejemplo, en categorías restringidas, he reflejado de cerca las clases estándar, PreArrowcomo la clase de categorías monoidales cartesianas, pero deliberadamente me mantuve arrfuera de él y no lo hice específico para Hask , porque eso reduce demasiado las capacidades de la categoría y hace que sea casi equivalente a Hask -Kleisli.