Anyone mind proofing a short monad transformers explanation?

I sent this to a friend who asked me about monad transformers and he reckons it should be saved somewhere. If anyone feels up to giving it a quick fact-check, that'd be great. I'm not sure what to do with it, though. It doesn't seem to be made of the right stuff for a tutorial but I'm not sure what to do with it. --- SNIP --- Basically it's like making a double, triple, quadruple, ... monad by wrapping around existing monads that provide wanted functionality. You have an innermost monad (usually Identity or IO but you can use any monad). You then wrap monad transformers around this monad to make bigger, better monads. Concrete example: Suppose I was writing a server. Each client thread must be of type IO () (that's because forkIO :: IO () -> IO ThreadID)). Suppose also that this server has some configuration that (in an imperative program) would be global that the clients all need to query.
data Config = Config Foo Bar Baz
One way of doing this is to use currying and making all the client threads of type Config -> IO (). Not too nice because any functions they call have to be passed the Config parameter manually. The Reader monad solves this problem but we've already got one monad. We need to wrap IO in a ReaderT. The type constructor for ReaderT is ReaderT r m a, with r the shared environment to read from, m the inner monad and a the return type. Our client_func becomes:
client_func :: ReaderT Config IO ()
We can then use the ask, asks and local functions as if Reader was the only Monad: (these examples are inside do blocks)
p <- asks port
(Assuming some function port :: Config -> Int or similar.) To do stuff in IO (or in the general case any inner monad) the liftIO function is used to make an IO function work in this wrapped space: (given h :: Handle, the client's handle)
liftIO $ hPutStrLn h "You lose" liftIO $ hFlush h
IO is once again special. For other inner monads, the lift function does the same thing. Note also that IO has no transformer and must therefore always be the innermost monad. This is all well and good, but the client_func now has type ReaderT Config IO () and forkIO needs a function of type IO (). The escape function for Reader is runReader :: Reader r a -> r -> a and similarly for ReaderT the escape function is runReaderT :: ReaderT r m a -> r -> m a: (Given some c :: Config that's been assembled from config files or the like)
forkIO (runReaderT client_func c)
Will do the trick. Monad transformers are like onions. They make you cry but you learn to appreciate them. Like onions, they're also made of layers. Each layer is the functionality of a new monad, you lift monadic functions to get into the inner monads and you have transformerised functions to unwrap each layer. They're also like a present in that regard: in this example we unwrapped the outer wrapping paper to get to the present: an object of type IO (), which lets us make haskell do something.

On 12/17/07, Jack Kelly
liftIO $ hPutStrLn h "You lose" liftIO $ hFlush h
IO is once again special. For other inner monads, the lift function does the same thing. Note also that IO has no transformer and must therefore always be the innermost monad.
Actually, this isn't true. In the case of ReaderT Config IO (), liftIO is the same as lift. liftIO exists because it is more general; it works for any monad that is an instance of "MonadIO", which includes IO, ReaderT r IO, StateT s IO, ReaderT r (StateT s (ErrorT e IO))), etc. In the last case, you could write lift $ lift $ lift $ hPutStrLn h "You lose" but it's much simpler to write liftIO $ hPutStrLn h "You lose" Similarily, "ask" is defined in the MonadReader typeclass, which includes Reader, ReaderT IO, and all sorts of other monads that include "Reader" at some level; only the real "reader" monad has a full implementation; the rest are defined in terms of "lift" or simpler operations, like so: instance MonadReader r m => MonadReader r (StateT s m) where ask = lift ask local f m = StateT $ \s -> local f (runStateT m s) -- ryan

Ryan Ingram wrote:
On 12/17/07, *Jack Kelly*
mailto:endgame.dos@gmail.com> wrote: > liftIO $ hPutStrLn h "You lose" > liftIO $ hFlush h
IO is once again special. For other inner monads, the lift function does the same thing. Note also that IO has no transformer and must therefore always be the innermost monad.
Actually, this isn't true. In the case of ReaderT Config IO (), liftIO is the same as lift.
Where can I find proofs that the monad transformers found in the Haskell libraries indeed produce monads as results? There should be a general construction and proof (eg. based on adjoint functor compositionality) but couldn't find it yet. Looking at "Monads and Effects" (Benton et al, LNCS 2395), for instance, I don't see any foundations discussed beyond section 6. Is this somewhere else? jno (www.di.uminho.pt/~jno)
participants (3)
-
J.N. Oliveira
-
Jack Kelly
-
Ryan Ingram