haskell - 为什么静态箭头概括了箭头？

Question

众所周知，Applicative概括 Arrows .在 Idioms are oblivious, arrows are meticulous, monads are promiscuous Sam Lindley、Philip Wadler 和 Jeremy Yallop 的论文据说 Applicative等价于静态箭头，即具有以下同构的箭头:arr a b :<->: arr () (a -> b)据我所知，它可以通过以下方式说明:
注:newtype Identity a = Id { runId :: a } . Klesli Identity是一个静态箭头，因为它包裹着 k :: a -> Identity b .同构只是删除或添加包装器。Kleilsi Maybe不是静态箭头，因为 k = Kleisli (const Nothing)存在 - 所有 f :: a -> b s 对应于 Just . f ，并且没有 k 的位置在同构中。
但同时两者Kleisli Identity和 Kleisli Maybe是 Arrow实例。因此，我看不出泛化是如何工作的。
在 Haskell/Understanding Arrows tutorial在 Wikibooks他们say static morphism和 note the following :

Those two concepts are usually known as static arrows and Kleisli arrows respectively. Since using the word "arrow" with two subtly different meanings would make this text horribly confusing, we opted for "morphism", which is a synonym for this alternative meaning.

这是我迄今为止唯一的线索 - 我是否混淆了 Haskell Arrow和箭头？
那么，这种层次结构是如何运作的呢？这是怎么回事Applicative的属性(property)形式化/证明？

Answer 1

我相信“概括”这个词会让你误入歧途。如 k是 Arrow ，确实是这样:

k x对于任何 x将是 Applicative ;

特别是k ()将是一个应用程序；

然后可以将该应用程序重新旋转为等效的静态箭头(根据 Static from semigroupoids ， Static (k ()) a b ~ k () (a -> b) )

然而，这个过程在一般情况下并不是无损的:静态箭头 Static (k ())不一定等同于 k我们开始的箭头；不需要同构。换句话说，静态箭头不能概括箭头。如果我们定义一个 StaticArrow类，它将是 Arrow 的子类，而不是父类(super class)。
P.S.:在维基教科书的引文中，措辞只是一个强调问题。例如，虽然 Kleisli 箭头确实是 Hughes/Control.Arrow箭，大多数时候当人们谈论“Kleisli 箭”时，他们并不是在想 Arrow例如，但仅是关于它们如何是范畴中的态射，其中范畴律相当于某些 monad 的 monad 律。特别是，这足以构成维基教科书那一段中的讨论。