[Haskell-cafe] A different Maybe maybe

[ajb at spamcop.net]

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
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