Does each type have a unique catamorphism?

Question

Recently, I finally felt that I understand catamorphism. I wrote a few about them in a recent answer , but in short I would say that catamorphism for abstract tags in the process of recursively passing a value of this type with a matching pattern of this type in one function for each constructor of the type. Although I would welcome any corrections in this question or a longer version in the answer above, I think I have it more or less, and this is not a question of this question, just some kind of background.

As soon as I realized that the functions you pass to the catamorphism exactly correspond to the type constructors, and the arguments of these functions also correspond to the field types of these constructors, all this suddenly seems rather mechanical, and I do not see where there is room for maneuver for alternative implementations.

For example, I simply composed this stupid type, without a real concept of what its structure “means”, and brought catamorphism for it. I see no other way that I could define a common goal for this type:

data X abf = A Int b | B | C (fa) (X abf) | D a xCata :: (Int -> b -> r) -> r -> (fa -> r -> r) -> (a -> r) -> X abf -> r xCata abcdv = case v of A ix -> aix B -> b C fx -> cf (xCata abcdx) D x -> dx 

My question is, does each type have a unique catamorphism (before reordering the arguments)? Or are there counterexamples: types for which catamorphism cannot be defined, or types for which there are two different but equally acceptable catamorphisms? If there are no counterexamples (i.e., Catamorphism for a type is unique and trivially deducible), is it possible to get GHC to get some kind of specification for me that automatically does this drudgework?

Answer 1

Catamorphism associated with a recursive type can be obtained mechanically.

Suppose you have a recursively defined type that has several constructors, each of which has its own fate. I will take the OP example.

 data X abf = A Int b | B | C (fa) (X abf) | D a 

Then we can rewrite the same type, forcing each of them to be one, regardless of everything. The argument 0 ( B ) becomes one if we add a unit type () .

 data X abf = A (Int, b) | B () | C (fa, X abf) | D a 

Then we can reduce the number of constructors to one, using Either instead of several constructors. Below we just write infix + instead of Either for short.

 data X abf = X ((Int, b) + () + (fa, X abf) + a) 

At the level of the term, we know that we can rewrite any recursive definition as the form x = fx where fw = ... writing the explicit equation of the fixed point x = fx . At the type level, we can use the same method for recursive recursive types.

 data X abf = X (F (X abf)) -- fixed point equation data F abfw = F ((Int, b) + () + (fa, w) + a) 

Now note that we can autocopy an instance of a functor.

 deriving instance Functor (F abf) 

This is possible because in the source type, each recursive link is only in a positive position. If this fails, making F abf not a functor, then we cannot have a catamorphism.

Finally, we can write the cata type as follows:

 cata :: (F abfw -> w) -> X abf -> w 

Is this the type of OP xCata ? It. We need to apply only some type isomorphisms. We use the following algebraic laws:

 1) (a,b) -> c ~= a -> b -> c (currying) 2) (a+b) -> c ~= (a -> c, b -> c) 3) () -> c ~= c 

By the way, it is easy to remember these isomorphisms if we write (a,b) as the product a*b , unit () as 1 and a->b as the power b^a . Indeed, they become 1) c^(a*b) = (c^a)^b , 2) c^(a+b) = c^a*c^b, 3) c^1 = c .

Anyway, let's start rewriting the part F abfw -> w , only

  F abfw -> w =~ (def F) ((Int, b) + () + (fa, w) + a) -> w =~ (2) ((Int, b) -> w, () -> w, (fa, w) -> w, a -> w) =~ (3) ((Int, b) -> w, w, (fa, w) -> w, a -> w) =~ (1) (Int -> b -> w, w, fa -> w -> w, a -> w) 

Consider now the full type:

 cata :: (F abfw -> w) -> X abf -> w ~= (above) (Int -> b -> w, w, fa -> w -> w, a -> w) -> X abf -> w ~= (1) (Int -> b -> w) -> w -> (fa -> w -> w) -> (a -> w) -> X abf -> w 

What is really (renaming w=r ) the desired type

 xCata :: (Int -> b -> r) -> r -> (fa -> r -> r) -> (a -> r) -> X abf -> r 

The "standard" cata implementation is

 cata g = wrap . fmap (cata g) . unwrap where unwrap (X y) = y wrap y = X y 

It takes some effort to understand because of its generality, but it really is intended.

---

About automation: yes, it can be automated, at least in part. There is a recursion-schemes package for hacking that allows one to write something like

 type X abf = Fix (F afb) data F abfw = ... -- you can use the actual constructors here deriving Functor -- use cata here 

Example:

 import Data.Functor.Foldable hiding (Nil, Cons) data ListF ak = NilF | ConsF ak deriving Functor type List a = Fix (ListF a) -- helper patterns, so that we can avoid to match the Fix -- newtype constructor explicitly pattern Nil = Fix NilF pattern Cons a as = Fix (ConsF a as) -- normal recursion sumList1 :: Num a => List a -> a sumList1 Nil = 0 sumList1 (Cons a as) = a + sumList1 as -- with cata sumList2 :: forall a. Num a => List a -> a sumList2 = cata h where h :: ListF aa -> a h NilF = 0 h (ConsF as) = a + s -- with LambdaCase sumList3 :: Num a => List a -> a sumList3 = cata $ \case NilF -> 0 ConsF as -> a + s 

Answer 2

Catamorphism (if it exists) is unique by definition . In category theory, catamorphism denotes a unique homomorphism from an initial algebra to some other algebra. As far as I know in Haskell, all catamorphisms exist because Haskell types form a Cartesian closed category, where finite objects, all products, and all exponents exist. See also Bartosh Milevsky 's blog post on F-algebras , which provides a good introduction to the topic.