Hello, Your definition for Bool reminds me a bit of the definition for booleans in Robert Dockins pure, untyped lambda calculus evaluator: http://www.eecs.tufts.edu/~rdocki01/lambda/prelude.lam http://www.eecs.tufts.edu/~rdocki01/lambda.html j.

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

Hey, welcome to to the group who have reinvented Church encoding of data types. :) -- Lennart On Mar 7, 2007, at 22:32 , 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

Comments are appreciated.

Greetings from my holidays, Joachim

-- Joachim "nomeata" Breitner mail: mail@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: joachimbreitner@amessage.de | http://www.joachim-breitner.de/ Debian Developer: nomeata@debian.org _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

G'day all. Quoting Joachim Breitner :

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