wren ng thornton wren at community.haskell.org
Fri Apr 16 01:13:30 EDT 2010

```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.  :-)
>
>     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)

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
```