<p>The problem with your counterexample is that the type you presented is not a valid instance of <code>ArrowApply</code> as far as I can tell.</p>

<p>You didn't present what the implementation of <code>app</code> 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.</p>

<p>What definition of <code>app</code> did you have in mind?</p>

CC BY-SA 3.0
2016-01-12T18:34:53.433Z
So you're saying that I have discovered here that I'll never find a valid instance of `ArrowApply` (because if I'd find one, then I'd have the equivalence)? I don't quite understand, since it already doesn't match on the type level. True, `app` might not satisfy the laws, but then the only consequence can be that the corresponding `ArrowMonad` will break the monad laws, right? But as I've presented, it wouldn't even typecheck! And that's strange, because it is possible to define _some_ (incorrect) instance of `app`.
Turion
CC BY-SA 3.0
2016-01-12T21:27:45.353Z
I'm not quite following what you're saying. What do you mean by "doesn't match on the type level"? That the types are not isomorphic?
Max New
CC BY-SA 3.0
2016-01-12T21:30:59.323Z
The precise relationship between ArrowApply and Monad is presented here: http://homepages.inf.ed.ac.uk/wadler/papers/arrows-and-idioms/arrows-and-idioms.pdf . The result (for which detailed proofs are elided) is that law-abiding ArrowApply types are exactly those where there is a type isomorphism between `a ~> b` and `a -> (1 ~> b)`.
Max New
CC BY-SA 3.0
2016-01-12T22:08:35.490Z
Right, I meant that the types are not isomorphic. But I was mistaken, I see. With an incorrect implementation of `app`, as in my case, there are still morphisms from the (incorrect) `ArrowApply` instance to the monad and vice versa, but they don't form an equivalence of types, as you say. Thanks for the reference!
Turion
CC BY-SA 3.0
2016-01-12T17:13:51.153Z
2016-01-12T17:13:51.153Z
Max New
<p>It is stated e.g. <a href="https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Arrow.html#t:ArrowMonad" rel="nofollow">on Hackage</a>, that the <code>ArrowApply</code> and the <code>Monad</code> typeclasses are equivalent. I have my doubts about this.</p>

<p>It is obvious that there are morphisms from <code>ArrowApply</code> to <code>Monad</code> and back, and one can check that one can prove the <code>Monad</code> laws and the <code>ArrowApply</code> laws in each case. What I doubt is that these morphisms are inverses.</p>

<p>They are defined this way:</p>

<ul>
<li>Let $\leadsto: \operatorname{Type} \times \operatorname{Type} \to \operatorname{Type}$ be an instance of <code>ArrowApply</code>, 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.</li>
<li>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.</li>
<li>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 <code>ArrowApply</code>.</li>
</ul>

<p>I cannot see at all that these constructions are inverse to each other. Here is what I believe to be a counter-example:</p>

<p>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. <a href="https://wiki.haskell.org/Yampa" rel="nofollow">Yampa</a>.</p>

<p>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.</p>

<p>Are <code>ArrowApply</code> and <code>Monad</code> inequivalent then, since the constructions aren't inverses of each other? Or is there another construction that makes them equivalent?</p>

<data-streams><haskell><monad><equivalence>
Are the `ArrowApply` and `Monad` typeclasses equivalent?
Turion
# Are the `ArrowApply` and `Monad` typeclasses equivalent?

(Asked by: username_0 on 2015-08-12)

It is stated e.g. [on Hackage](https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Arrow.html#t:ArrowMonad), 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](https://wiki.haskell.org/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?

**Tags:** data-streams, haskell, monad, equivalence


---

## 1 answers

### Answer by username_1 on 2016-01-12. Score: 1 | Accepted answer

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?

> **Comments:**
> **username_0**: So you're saying that I have discovered here that I'll never find a valid instance of `ArrowApply` (because if I'd find one, then I'd have the equivalence)? I don't quite understand, since it already doesn't match on the type level. True, `app` might not satisfy the laws, but then the only consequence can be that the corresponding `ArrowMonad` will break the monad laws, right? But as I've presented, it wouldn't even typecheck! And that's strange, because it is possible to define _some_ (incorrect) instance of `app`.  
> **username_1**: I'm not quite following what you're saying. What do you mean by "doesn't match on the type level"? That the types are not isomorphic?  
> **username_1**: The precise relationship between ArrowApply and Monad is presented here: http://homepages.inf.ed.ac.uk/wadler/papers/arrows-and-idioms/arrows-and-idioms.pdf . The result (for which detailed proofs are elided) is that law-abiding ArrowApply types are exactly those where there is a type isomorphism between `a ~> b` and `a -> (1 ~> b)`.  
> **username_0**: Right, I meant that the types are not isomorphic. But I was mistaken, I see. With an incorrect implementation of `app`, as in my case, there are still morphisms from the (incorrect) `ArrowApply` instance to the monad and vice versa, but they don't form an equivalence of types, as you say. Thanks for the reference!  

---

