G'day all.
Quoting Joachim Breitner
This is probably nothing new, but was offline at the time of writing, so I didn?t check.
One more thing. As you've probably worked out, one way to construct the Church encoding of a type is to realise that the only thing that you can really do with an algebraic data type is do a case-switch on it. Taking Maybe as the example: just :: a -> Maybe a nothing :: Maybe a And a function caseMaybe such that: caseMaybe (just x) j n = j x caseMaybe (nothing) j n = n You can obtain the Church encoding by defining caseMaybe to be id: just x j n = j x nothing j n = n caseMaybe = id You can work out the type of Maybe in the Church encoding by type checking just and nothing, or you can get it straight from the "data" declaration of Maybe. What you may not have realised, is that you can get monad transformers the same way, by explicitly stating that the return type of the continuation is in the underlying monad. As you probably know, Maybe is a monad: type Maybe a = forall b. (a -> b) -> b -> b just x = \j n -> j x nothing = \j n -> n fail _ = nothing return = just (m >>= k) = \j n -> m (\x -> k x j n) n Introduce a monad, m, and replace b by "m b": type MaybeT m a = forall b. (a -> m b) -> m b -> m b justT x = \j n -> j x nothingT = \j n -> n fail _ = nothingT return = justT (m >>= k) = \j n -> m (\x -> k x j n) n lift m = \j n -> m >>= j ...and you have an instant monad transformer. A Maybe transformer is like ErrorT, only without an error message. As an exercise, try this with List: type List a = forall b. (a -> b -> b) -> b -> b type ListT m a = forall b. (a -> m b -> m b) -> m b -> m b If you get stuck, this (unsurprisingly) is the same type as Ralf Hinze's backtracking monad transformer. Cheers, Andrew Bromage