[Haskell-cafe] A different Maybe maybe
Stefan O'Rear
stefanor at cox.net
Wed Mar 7 18:36:35 EST 2007
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
More information about the Haskell-Cafe
mailing list