Are the `ArrowApply` and `Monad` typeclasses equivalent? 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?
The problem with your counterexample is that the type you presented is not a valid instance of ArrowApply as far as I can tell.

You didn't present what the implementation of app but the only one I could come up with (where you use the input stream function once and then discard it) doesn't satisfy the 2nd and 3rd ArrowApply laws.

What definition of app did you have in mind?