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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
