It is stated e.g. on Hackage, that the ArrowApply and the Monad typeclasses are equivalent. I have my doubts about this.
It is obvious that there are morphisms from ArrowApply to Monad and back, and one can check that one can prove the Monad laws and the ArrowApply laws in each case. What I doubt is that these morphisms are inverses.
They are defined this way:
- Let $\leadsto: \operatorname{Type} \times \operatorname{Type} \to \operatorname{Type}$ be an instance of
ArrowApply, so there is $arr: (a \to b) \to (a \leadsto b)$, $first: (a \leadsto b) \to (a \times c \leadsto b \times c)$ and $app: ((b \leadsto c) \times b) \leadsto c$, and $\leadsto$ is the hom of some category. I'm leaving out the universal quantifiers on lower-case letters, like in Haskell-style. - We define a monad $m: \operatorname{Type} \to \operatorname{Type}$ by $m a = 1 \leadsto a$. For example, $\operatorname{return}: a \to m a$ is defined as $\operatorname{return} x = arr (\lambda y. x)$, and $\operatorname{join}$ and the monad laws are not very hard.
- Or the other way: Given a monad $m$, define $a \leadsto b = a \to m b$. This defines obviously a category and also gives rise to an
ArrowApply.
I cannot see at all that these constructions are inverse to each other. Here is what I believe to be a counter-example:
Define your arrow type as the fixpoint of $a \leadsto b = a \to (b \times (a \leadsto b))$. This is the terminal coalgebra of the functor $x \mapsto A \to (b \times x)$. It represents a stateful, causal stream function. Constructions like this are used in functional reactive programming, e.g. Yampa.
We then define the monad $m$ in terms of $\leadsto$. Intuitively, $m a$ is the type of stream functions from unit to $a$, in other words, streams in $a$. But Kleisli arrows of this monad aren't stream functions: $$m a = 1 \to a \times (1 \leadsto a) \cong a \times (m a)$$ $$\implies a \to m b \simeq a \to b \times (m b) \not\simeq a \to b \times (a \leadsto b) \simeq a \leadsto b$$ So in this case, the constructions are not equivalent, if I haven't made a mistake somewhere.
Are ArrowApply and Monad inequivalent then, since the constructions aren't inverses of each other? Or is there another construction that makes them equivalent?
