# [Haskell-cafe] A different Maybe maybe

ajb at spamcop.net ajb at spamcop.net
Fri Mar 9 05:57:57 EST 2007

```G'day all.

Quoting Joachim Breitner <mail at joachim-breitner.de>:

> 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

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