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:
Note: newtype Identity a = Id { runId :: a }.
Klesli Identity is a Static Arrow as it wraps k :: a -> Identity b. Isomorphism just removes or adds the wrapper.
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.
But at the same time both Kleisli Identity and Kleisli Maybe are Arrow instances. Therefore, I can not see how the generalisation works.
In Haskell/Understanding Arrows tutorial on Wikibooks they say static morphism and 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.
That is the only lead I have so far - am I confusing Haskell Arrow and arrows?
So, how does this hierarchy work? How is this Applicative's property formalised/proven?
I believe the word "generalises" is leading you astray. If k is an Arrow, it is indeed the case that:
k x for any x will be an Applicative;k () will be an applicative;Static from semigroupoids, Static (k ()) a b ~ k () (a -> b))This process, however, is not lossless in the general case: the static arrow Static (k ()) is not necessarily equivalent to the k 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.: 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.