Move MonadIO to base

[wren ng thornton]

Anders Kaseorg wrote:
> On Tue, 13 Apr 2010, Anders Kaseorg wrote:
>> The striking similarity between instances of MonadCatchIO suggests to me 
>> that something deeper is going on.  Is there a cleaner abstraction that 
>> captures this idea?
> 
> Here a possible answer.  I haven’t entirely figured out what it “means” 
> yet, but maybe someone who knows more category theory will be able to 
> figure that out.  :-)
> 
> class Monad m => MonadMorphIO m where
>     morphIO :: (forall b. (m a -> IO b) -> IO b) -> m a


This is broadly related to Church encoding and CPS conversion. For 
example sums, products, and recursion can be encoded via:

     (forall r. (X->r) -> (Y->r) -> r)
         ~= X+Y
         == Either X Y
     (forall r. (X->Y->r) -> r)
         ~= X*Y
         == (X,Y)
     (forall r. (X->r->r) -> r -> r)
         == (forall r. (X->r->r) -> (()->r) -> r)
         ~= fix r. X*r + 1
         == [X]

So if we ignore the IO parts, then your class is isomorphic to

     newtype F m a = MkF (m a)

     class Monad m => MonadMorphIO where
         morphIO  :: F m a -> m a

But that's ignoring the IO. So what is this class saying, with the IO? 
Well, what does (m a -> IO b) mean? One view treats IO as merely a type 
constructor, in which case it means ((_->_) (m a) (IO b)), i.e. a 
morphism in Hask from (m a) to (IO b). But since IO is a monad we could 
also think of the Kleisli category generated by IO, in which case it 
means ((_ -> IO _) (m a) b), i.e. a morphism in the IO category from (m 
a) to b.

Putting these together, your class means: if you can construct/eliminate 
an (F m a) in the IO category, then you can construct an (m a) in the 
Hask category. I.e., IO(m a) is a subset of (m a).

-- 
Live well,
~wren