[Haskell-cafe] A different Maybe maybe

[Stefan O'Rear]

On Wed, Mar 07, 2007 at 11:32:08PM +0100, Joachim Breitner wrote:
> [Also on http://www.joachim-breitner.de/blog/archives/229-A-different-Maybe-maybe.html]
> 
> Hi,
> 
> For a while I have been thinking: Isn???t there a way to get rid of the
> intermediate Maybe construct in a common expression like ???fromMaybe
> default . lookup???. It seems that a way to do that would be to pass more
> information to the Maybe-generating function: What to do with a
> Just-Value, and what to return in case of Nothing. This leads to a new
> definion of the Maybe data type as a function. Later I discovered that
> this seems to work for any algebraic data type.
> 
> This is probably nothing new, but was offline at the time of writing, so
> I didn???t check. This means that this might also be total rubbish. Enjoy.
> 
>       * ???Algebraic Data Type Done Differently??? (PDF-File) at
>         http://www.joachim-breitner.de/various/FunctionalMaybe.pdf
>       * ???Algebraic Data Type Done Differently??? (Literate Haskell Source)
>         at http://www.joachim-breitner.de/various/FunctionalMaybe.lhs

Congratulations!  You've just reinvented Church encoding.  Indeed,
calculi such as the untyped lambda calculus and the rankN typed System
F omit algebraic datatypes precisely because of the possibility of
Church encoding. 

Some more examples:  (|~| x . type is system-f syntax for forall x . type):

data Bool = False | True            --> |~| r . r -> r -> r         (AKA church booleans)
data Nat = Z | S Nat                --> |~| r . r -> (r -> r) -> r  (AKA church numerals, recursive)
data Maybe x = Nothing | Just x     --> \x::* . |~| r . r -> (x -> r) -> r (Fw)
data List x = Nil | Cons x (List x) --> \x::* . |~| r . r -> (x -> r -> r) -> r (Fw, recursive)
data Mu f = Mu (f (Mu f))           --> \f::*->* . |~| r . (f r -> r) -> r (Fw, induction)

There are also coinductive translations for recursion:

data Nat = Z | S Nat                --> |~| r . (|~| s . s -> (s -> Maybe s) -> r) -> r
data List x = Nil | Cons x (List x) --> \x::* . |~| r . (|~| s . s -> (s -> Either s (s, x)) -> r) -> r
data Mu f = Mu (f (Mu f))           --> \f::*->* . |~| r . (|~| s . s -> (s -> f s) -> r) -> r