[Haskell-cafe] Anyone mind proofing a short monad transformers explanation?

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)