与 Arrow 和 Applicative 不同，为什么互让让 ArrowApply 和 Monads 等价？

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.

widely known 是 ArrowApply 实例产生一个 Monad，反之亦然：

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

在我偶然发现上面提到的post 之前，我觉得这个sn-p 是ArrowApply 和Monad 类等价的合理证明。然而，知道Arrow and Applicative are not, in fact, equivalent 和下面的sn-p 让我对Monad 和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.

写下来的例子很明显，但我无法理解通过 Monad 的“往返”如何保留所有 ArrowApply 功能，因为最初我们有一个取决于某些输入的箭头 (a b c) 但在最后，我们最终得到一个强制进入包装器的箭头，该包装器的输入类型为单位类型 (ArrowMonad (a () b))。

很明显我在这里做错了什么，但我无法理解到底是什么。

ArrowApply 和 Monad 等价的完整证据是什么？

Arrow 和 Applicative 不等价的例子说明了什么？一个人能概括另一个人吗？

箭头演算和范畴论对整个情况的解释是什么？

我将不胜感激完整的解释和提示，它们可以帮助人们自己拟定一份似是而非的证据。

Answer 1

因为最初我们有一个依赖于某些输入 (a b c) 的箭头，但最后，我们最终将一个箭头强制到一个以单位类型作为其输入类型 (ArrowMonad (a () b)) 的包装器中

我想这是混乱的中心点，而且确实令人困惑。我喜欢认为箭头主要是笛卡尔幺半群类别中的态射，你不会得到这个，但由于arr，Arrow 类实际上比这更严格——它为你提供了一个来自 Hask 进入该类别。但是，有点令人惊讶的是，这也需要您在 other 方向上得到一个映射：任何箭头都可以替换为一个 function，它只产生一个平凡域的箭头。具体来说，

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

好吧，仅此一点并不会太令人震惊——也许我们只是在这里丢弃了一些信息？ – 但对于ArrowApply，这实际上是一个同构：你可以通过

找回原来的箭头

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

...这正是 Monad (ArrowMonad a) 实例中使用的内容。

所以结果是：arr，通过要求您可以在类别中嵌入任何 Haskell 函数，强制该类别基本上归结为 带有一些结果包装器的函数，IOW 一些东西像 Kleisli 箭。

查看其他一些类别理论层次结构，看看这不是笛卡尔幺半群类别的基本特征，而是 Hask 的产物 → k 函子。例如。 in constrained-categories 我已经密切反映了标准类，PreArrow 是笛卡尔幺半群类别的类，但故意将 arr 排除在外，并且没有使其特定于 Hask，因为这会过多地降低类别的功能，并导致它几乎等同于 Hask-Kleisli。