[Haskell-cafe] Anyone mind proofing a short monad transformers
jno at di.uminho.pt
Tue Apr 22 09:09:37 EDT 2008
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?
More information about the Haskell-Cafe