[Haskell-cafe] Re: Church Encoding Function

[Lennart Augustsson]

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 at joachim-breitner.de
>   Homepage: http://www.joachim-breitner.de
>   ICQ#: 74513189
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe