[Haskell-cafe] Re: Church Encoding Function

[Derek Elkins]

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.