Hi, some more ideas following from the last post. I noticed how the function Data.Maybe.maybe converts a Haskell Maybe into a Church encoded Maybe. Also, the if construct, interpreted as a function, converts a Bool into a church encoded Bool. If lists are encoded as forall b. (a -> b -> b) -> b -> b, then foldr, with the right order of arguments, converts a haskell [] to a Church encoded List. Is there a name for these functions? “Characteristic Church Encoding Functions” maybe? Are there more than these: Maybe -- maybe Bool -- ifthenelse List -- foldr (,) -- uncurry Just a short idea while waiting at the airport... Greetings, 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
On Saturday 10 March 2007 09:43, Joachim Breitner wrote:
Hi,
some more ideas following from the last post. I noticed how the function Data.Maybe.maybe converts a Haskell Maybe into a Church encoded Maybe. Also, the if construct, interpreted as a function, converts a Bool into a church encoded Bool.
If lists are encoded as forall b. (a -> b -> b) -> b -> b, then foldr, with the right order of arguments, converts a haskell [] to a Church encoded List.
Is there a name for these functions? “Characteristic Church Encoding Functions” maybe? Are there more than these:
I believe these are the same as catamorphisms. http://en.wikipedia.org/wiki/Catamorphism Here is the paper where the term (AFAIK) was coined (although I have to admit to having only skimmed it): http://citeseer.ist.psu.edu/meijer91functional.html I'm pretty sure you can define a catamorphism for any regular algebraic data type. I'm not 100% sure what the story is for non-regular (AKA nested) datatypes.
Maybe -- maybe Bool -- ifthenelse List -- foldr (,) -- uncurry
Just a short idea while waiting at the airport...
Greetings, Joachim
Hi, Am Samstag, den 10.03.2007, 14:52 -0500 schrieb Stefan Monnier:
I'm pretty sure you can define a catamorphism for any regular algebraic data type.
Actually, so-called negative occurrences in (regular) data types cause problems. Try to define the catamorphism of
data Exp = Num Int | Lam (Exp -> Exp) | App Exp Exp
to see the problem,
I guess Robert is still true as this Exp contains a non-algebraic type ((->)), therefore is not a regular algebraic type. (Based on an assumed meaning of “algebraic data type”). But let’s see... Am I right to assume that I have found a catamorphism if and only if the that function, applied to the data type constructors (in the right order) gives me the identity on this data type? maybe Nothing Just == id :: Maybe -> Maybe \b -> if b then True else False == id :: Bool -> Bool foldr (:) [] == id :: [a] -> [a] uncurry (,) == id :: (a,b) -> (a,b) either Left Right == id :: Either a b -> Either a b Does that also mean that catamorphism for a given type are unique (besides argument re-ordering)? Now some brainstorming about the above Exp. I guess we want: exp Num Lam App e == id e therefore exp :: (Int -> Exp) ((Exp -> Exp) -> Exp) (Exp -> Exp -> Exp) Exp now we want the return type to not matter exp :: forall b. (Int -> b) ((Exp -> Exp) -> b) (Exp -> Exp -> b) Exp So my guess would be: exp f _ _ (Num i) = f i exp _ f _ (Lam g) = f g exp _ _ f (App e1 e2) = f e1 e2 Looks a bit stupid, but seems to work, especially as there is not much a function with type (Exp -> Exp) -> b can do, at least on it’s own. Is that a catamorphism? Greetings, Joachim -- Joachim Breitner e-Mail: mail@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189
When you make these kind of elimination functions you have a choice. Namely if you want to do case analysis only, or primitive recursion. For non-recursive data types they come out the same, so 'maybe', 'either', 'uncurry', etc are the same. But for lists it differs: -- Case analysis caseList :: (a -> [a] -> r) -> r -> [a] -> r caseList c n [] = n caseList c n (x:xs) = c x xs And primitive recursion is foldr. It's easy to write the case analysis function for any data type; it just encodes what 'case' does. If you're in a language with general recursion there is no loss in expressive power by just having the case analysis functions instead of the primitive recursive ones since you can recurse yourself. But, in a language without Y you'd be stuck with boring functions with the likes of foldr. -- Lennart On Mar 11, 2007, at 08:27 , Joachim Breitner wrote:
Hi,
Am Samstag, den 10.03.2007, 14:52 -0500 schrieb Stefan Monnier:
I'm pretty sure you can define a catamorphism for any regular algebraic data type.
Actually, so-called negative occurrences in (regular) data types cause problems. Try to define the catamorphism of
data Exp = Num Int | Lam (Exp -> Exp) | App Exp Exp
to see the problem,
I guess Robert is still true as this Exp contains a non-algebraic type ((->)), therefore is not a regular algebraic type. (Based on an assumed meaning of “algebraic data type”). But let’s see...
Am I right to assume that I have found a catamorphism if and only if the that function, applied to the data type constructors (in the right order) gives me the identity on this data type?
maybe Nothing Just == id :: Maybe -> Maybe \b -> if b then True else False == id :: Bool -> Bool foldr (:) [] == id :: [a] -> [a] uncurry (,) == id :: (a,b) -> (a,b) either Left Right == id :: Either a b -> Either a b
Does that also mean that catamorphism for a given type are unique (besides argument re-ordering)?
Now some brainstorming about the above Exp. I guess we want: exp Num Lam App e == id e therefore exp :: (Int -> Exp) ((Exp -> Exp) -> Exp) (Exp -> Exp -> Exp) Exp now we want the return type to not matter exp :: forall b. (Int -> b) ((Exp -> Exp) -> b) (Exp -> Exp -> b) Exp So my guess would be: exp f _ _ (Num i) = f i exp _ f _ (Lam g) = f g exp _ _ f (App e1 e2) = f e1 e2 Looks a bit stupid, but seems to work, especially as there is not much a function with type (Exp -> Exp) -> b can do, at least on it’s own. Is that a catamorphism?
Greetings, Joachim
-- Joachim Breitner e-Mail: mail@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Joachim Breitner wrote:
Hi,
Am Samstag, den 10.03.2007, 14:52 -0500 schrieb Stefan Monnier:
I'm pretty sure you can define a catamorphism for any regular algebraic data type. Actually, so-called negative occurrences in (regular) data types cause problems. Try to define the catamorphism of
data Exp = Num Int | Lam (Exp -> Exp) | App Exp Exp
to see the problem,
I guess Robert is still true as this Exp contains a non-algebraic type ((->)), therefore is not a regular algebraic type. (Based on an assumed meaning of “algebraic data type”). But let’s see...
Am I right to assume that I have found a catamorphism if and only if the that function, applied to the data type constructors (in the right order) gives me the identity on this data type?
maybe Nothing Just == id :: Maybe -> Maybe \b -> if b then True else False == id :: Bool -> Bool foldr (:) [] == id :: [a] -> [a] uncurry (,) == id :: (a,b) -> (a,b) either Left Right == id :: Either a b -> Either a b
Does that also mean that catamorphism for a given type are unique (besides argument re-ordering)?
Now some brainstorming about the above Exp. I guess we want: exp Num Lam App e == id e therefore exp :: (Int -> Exp) ((Exp -> Exp) -> Exp) (Exp -> Exp -> Exp) Exp now we want the return type to not matter exp :: forall b. (Int -> b) ((Exp -> Exp) -> b) (Exp -> Exp -> b) Exp So my guess would be: exp f _ _ (Num i) = f i exp _ f _ (Lam g) = f g exp _ _ f (App e1 e2) = f e1 e2 Looks a bit stupid, but seems to work, especially as there is not much a function with type (Exp -> Exp) -> b can do, at least on it’s own. Is that a catamorphism?
Greetings, Joachim
Catamorphisms, folds, are the mediating arrows of initial algebras and thus are unique. I believe those equations combined with the free theorem that such functions would have, do guarantee that it would be that arrow.
On 3/10/07, Robert Dockins
I'm pretty sure you can define a catamorphism for any regular algebraic data type. I'm not 100% sure what the story is for non-regular (AKA nested) datatypes.
They do exist: Initial Algebra Semantics is Enough! Patricia Johann and Neil Ghani. http://crab.rutgers.edu/~pjohann/tlca07.pdf code: http://www.cs.nott.ac.uk/~nxg/Tlca07.hs Jim
On Sat, Mar 10, 2007 at 03:43:41PM +0100, Joachim Breitner wrote:
Hi,
some more ideas following from the last post. I noticed how the function Data.Maybe.maybe converts a Haskell Maybe into a Church encoded Maybe. Also, the if construct, interpreted as a function, converts a Bool into a church encoded Bool.
If lists are encoded as forall b. (a -> b -> b) -> b -> b, then foldr, with the right order of arguments, converts a haskell [] to a Church encoded List.
Is there a name for these functions? ???Characteristic Church Encoding Functions??? maybe? Are there more than these:
I usually hear "deconstructor". either :: Either a b -> (a -> r) -> (b -> r) -> r
Maybe -- maybe Bool -- ifthenelse List -- foldr (,) -- uncurry
Just a short idea while waiting at the airport...
Greetings, 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
On Sat, Mar 10, 2007 at 03:43:41PM +0100, Joachim Breitner wrote:
Hi,
some more ideas following from the last post. I noticed how the function Data.Maybe.maybe converts a Haskell Maybe into a Church encoded Maybe. Also, the if construct, interpreted as a function, converts a Bool into a church encoded Bool.
If lists are encoded as forall b. (a -> b -> b) -> b -> b, then foldr, with the right order of arguments, converts a haskell [] to a Church encoded List.
Is there a name for these functions?
folds (with the arguments flipped)
participants (9)
-
David House -
Derek Elkins -
Jim Apple -
Joachim Breitner -
Lennart Augustsson -
Robert Dockins -
Ross Paterson -
Stefan Monnier -
Stefan O'Rear