1
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Turion Jan 12 '16 at 18:34
  • $\begingroup$ 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? $\endgroup$ – Max New Jan 12 '16 at 21:27
  • 1
    $\begingroup$ The precise relationship between ArrowApply and Monad is presented here: homepages.inf.ed.ac.uk/wadler/papers/arrows-and-idioms/… . 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). $\endgroup$ – Max New Jan 12 '16 at 21:30
  • $\begingroup$ 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! $\endgroup$ – Turion Jan 12 '16 at 22:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.