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.htm...]
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