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

[J.N. Oliveira]

Ryan Ingram wrote:

> On 12/17/07, *Jack Kelly* <endgame.dos at gmail.com 
> <mailto:endgame.dos at 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)