[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.[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
properties about the identity monad (e.g., being both pointed and
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
parametricity when dealing with monads:
http://okmij.org/ftp/Computation/lem.html
--
Live well,
~wren
More information about the Haskell-Cafe
mailing list