[Haskell-cafe] Re: Move MonadIO to base

[wren ng thornton]

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