[Haskell-cafe] Re: Move MonadIO to base
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.
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
properties about the identity monad (e.g., being both pointed and
copointed) since it doesn't generalize to every monad in the way I
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...
 Oleg discusses a similar need to be careful about appeals to
parametricity when dealing with monads:
More information about the Haskell-Cafe