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