wren ng thornton wren at freegeek.org
Tue Apr 20 00:49:17 EDT 2010

```Anders Kaseorg wrote:
> Isaac Dupree wrote:
>> Do you see the difference? The effects are sequenced in different places.
>> The return/join pair moves all the effects *outside* the operations such
>> as catch... thus defeating the entire purpose of morphIO.
>
> Yes; my question is more whether Wren has a more clever way to get an
> isomorphism (forall b. (m a -> IO b) -> IO b) <-> IO (m a) that would make
> the simpler interface work out.  (Or maybe I misunderstood what he was
> getting at.)

Yeah no, that's what I was getting at. Since it doesn't quite work out,
I should probably rethink my appeal to parametricity re Kleisli arrows.[1]

That is, when we take the monad to be the identity monad or equivalently
to be "no monad", then parametricity yields: (forall b. (m a -> b) -> b)
<-> (m a). Apparently this makes some sort of appeal to special
copointed) since it doesn't generalize to every monad in the way I
suggested.

<musing>
Perhaps the correct version is this?

forall a n. Monad n =>
(forall b. (m a -> n b) -> n b) <-> n (m (n a))

Of course that may not solve your H98 concerns. Not all monads m provide
a universal law (forall n, n.m.n -> n.m) so to define the law you'd need
MPTCs to relate m and n. But if we monomorphize to just n=IO that would
simplify things; but then we'd need (Traversable m) in order to collapse
the two layers of IO...
</musing>

[1] Oleg discusses a similar need to be careful about appeals to