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.