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

Question

这是我要参考的 SO 帖子。此外，我将在该问题中使用与 OP 相同的片段，以免分离材料。

据众所周知的是一个ArrowApply实例产生一个单子，反之亦然：

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

在我偶然发现上面引用的帖子之前，我觉得这个片段是ArrowApply和Monad类等价的合理证明。然而，知道Arrow 和 Applicative 实际上并不等价，下面的代码片段让我对Monadand的完全等价证明感到好奇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

因此，如果您通过 applicative 往返，您将失去一些功能。

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

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

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

Arrow和Applicative解释不等价的例子是什么？一个人概括另一个人吗？

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

我将不胜感激可以帮助人们自己制定合理证据的完整解释和提示。

Answer 1

\n

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

\n

\n\n

我想这就是令人困惑的中心点，而且确实令人困惑。我喜欢将箭头视为笛卡尔幺半群范畴中的大部分态射，您不会得到这一点，但Arrow由于 \xe2\x80\x93 ，该类实际上已经比这更具限制性，它为您提供了一个从Hask到的arr函子类别。但是，有点令人惊讶的是，这还需要您获得另一个方向的映射：任何箭头都可以替换为仅产生平凡域箭头的函数。具体来说，

\n\n

arrAsFunction :: Arrow k => k x y -> (x -> k () y)\narrAsFunction \xcf\x86 x = \xcf\x86 <<< arr (const x)\n

\n\n

好吧，仅此一点并不会太具有开创性 \xe2\x80\x93 也许我们只是在这里丢弃了一些信息？\xe2\x80\x93 但这ArrowApply实际上是同构：您可以通过以下方式取回原始箭头

\n\n

retrieveArrowFromFunction :: \xe2\x88\x80 k x y .\n          ArrowApply k => (x -> k () y) -> k x y\nretrieveArrowFromFunction f = arr f\' >>> app\n where f\' :: x -> (k () y, ())\n       f\' x = (f x, ())\n

\n\n

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

\n\n

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

\n\n

查看其他一些范畴论层次结构，您会发现这不是笛卡尔幺半群范畴的基本特征，而实际上是Hask \xe2\x86\x92 k函子的产物。例如，在约束类别中，我已经密切反映了标准类，如PreArrow笛卡尔幺半群类别，但故意将arr其排除在外，并且没有使其特定于Hask，因为这会降低类别的功能太多并导致它几乎等同于Hask -Kleisli。

\n