为什么静态箭头会泛化箭头? [英] Why do Static Arrows generalise Arrows?

问题描述

众所周知，Applicative概括了Arrows.在惯用语是忽略的，箭头是细致的， Sam Lindley，Philip Wadler和Jeremy Yallop写的monads是混杂的论文，据说Applicative等效于Static Arrows，即具有以下同构性的箭头:

It is widely known that Applicative generalises Arrows. In the Idioms are oblivious, arrows are meticulous, monads are promiscuous paper by Sam Lindley, Philip Wadler and Jeremy Yallop it is said that Applicative is equivalent to Static Arrows, that is arrows for which the following isomorphism holds:

arr a b :<->: arr () (a -> b)

据我了解，可以通过以下方式进行说明:

As far as I can understand, it could be illustrated the following way:

注意:newtype Identity a = Id { runId :: a }.

Note: newtype Identity a = Id { runId :: a }.

Klesli Identity是静态箭头，因为它包装了k :: a -> Identity b.同构只是删除或添加包装.

Klesli Identity is a Static Arrow as it wraps k :: a -> Identity b. Isomorphism just removes or adds the wrapper.

Kleilsi Maybe不是静态箭头，因为存在k = Kleisli (const Nothing)-所有f :: a -> b都与Just . f相对应，并且k在同构中没有位置.

Kleilsi Maybe is not a Static Arrow as k = Kleisli (const Nothing) exists - all f :: a -> bs correspond to Just . f, and there is no place for k in the isomorphism.

但同时Kleisli Identity和Kleisli Maybe都是Arrow实例.因此，我看不到泛化的原理.

But at the same time both Kleisli Identity and Kleisli Maybe are Arrow instances. Therefore, I can not see how the generalisation works.

在说静态态射 和

这两个概念通常分别称为静态箭头和Kleisli箭头.由于使用单词箭头"，因此具有两种微妙的含义会使该文本令人震惊，我们选择了形态"，它是这种替代含义的同义词.

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和箭头吗?

That is the only lead I have so far - am I confusing Haskell Arrow and arrows?

那么，该层次结构如何工作? Applicative的财产如何形式化/证明?

So, how does this hierarchy work? How is this Applicative's property formalised/proven?

推荐答案

我相信"generalises"一词的含义是使你误入歧途.如果arr是Arrow，则确实是这样:

I believe the word "generalises" is leading you astray. If arr is an Arrow, it is indeed the case that:

任何x的
• arr x将是Applicative;
• 尤其是arr ()将是可应用的；
• 然后可以将该应用程序重新翻译为等效的静态箭头(根据

• arr x for any x will be an Applicative;
• In particular, arr () will be an applicative;
• That applicative can then be respun as an equivalent static arrow (in terms of Static from semigroupoids, Static (arr ()) a b ~ arr () (a -> b))

但是，在一般情况下，此过程并非无损:静态箭头Static (arr ())不一定等同于我们开始使用的arr箭头；不需要同构.换句话说，静态箭头不能概括箭头.如果要定义StaticArrow类，它将是Arrow的子类，而不是超类.

This process, however, is not lossless in the general case: the static arrow Static (arr ()) is not necessarily equivalent to the arr arrow we started with; there need not be an isomorphism. In other words, static arrows do not generalise arrows. If we were to define a StaticArrow class, it would be a subclass of Arrow, and not a superclass.

P.S .:在Wikibook上引用时，措词只是一个强调的问题.例如，虽然Kleisli箭头的确是Hughes/Control.Arrow箭头，但是大多数时候人们在谈论"Kleisli箭头"时，他们不是在考虑Arrow实例，而只是在考虑它们在类别中的变态，其中类别定律等于某个单子的单子定律.特别是，这足以在Wikibook的那段文章中进行讨论.

P.S.: On the Wikibook quote, the phrasing there is just a matter of emphasis. For instance, while Kleisli arrows are indeed Hughes/Control.Arrow arrows, most of the time when people talk of "Kleisli arrows" they are not thinking about the Arrow instance, but merely about how they are morphisms in a category in which the category laws amount to the monad laws for some monad. In particular, that suffices to frame the discussion in that passage of the Wikibook.

这篇关于为什么静态箭头会泛化箭头?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！