What's the type of a catamorphism (fold) for non-regular recursive types?

Question

Many catamorphisms seem to be simple enough, mostly replacing each data constructor with a custom function, e.g.

data Bool = False | True
foldBool :: r              -- False constructor
         -> r              -- True constructor
         -> Bool -> r

data Maybe a = Nothing | Just a
foldMaybe :: b             -- Nothing constructor
          -> (a -> b)      -- Just constructor
          -> Maybe a -> b

data List a = Empty | Cons a (List a)
foldList :: b              -- Empty constructor
         -> (a -> b -> b)  -- Cons constructor
         -> List a -> b

However, what's not clear to me is what happens if the same type constructor is used, but with a different type argument. E.g. instead of passing a List a to Cons, what about

data List a = Empty | Cons a (List (a,a))

Or, maybe a more crazy case:

data List a = Empty | Cons a (List (List a))
foldList :: b              -- Empty constructor
         -> ???            -- Cons constructor
         -> List a -> b

The two plausible ideas I have for the ??? part are

• (a -> b -> b), i.e. replacing all applications of the List constructor recursively)
• (a -> List b -> b), i.e. merely replacing all List a applications.

Which of the two would be correct - and why? Or would it be something different altogether?

Answer 1

This is a partial answer, only.

The issue the OP raises is: how to define fold/cata in the case of non-regular recursive types?

Since I don't trust myself in getting this right, I will resort to asking Coq instead. Let's start from a simple, regular recursive list type.

Inductive List (A : Type) : Type :=
  | Empty: List A
  | Cons : A -> List A -> List A
.

Nothing fancy here, List A is defined in terms of List A. (Remember this -- we'll get back to it.)

What about the cata? Let's query the induction pinciple.

> Check List_rect.
forall (A : Type) (P : List A -> Type),
   P (Empty A) ->
   (forall (a : A) (l : List A), P l -> P (Cons A a l)) ->
   forall l : List A, P l

Let's see. The above exploits dependent types: P depends on the actual value of the list. Let's just manually simplify it in the case P list is a constant type B. We obtain:

forall (A : Type) (B : Type),
   B ->
   (forall (a : A) (l : List A), B -> B) ->
   forall l : List A, B

which can be equivalently written as

forall (A : Type) (B : Type),
   B ->
   (A -> List A -> B -> B) ->
   List A -> B

Which is foldr except that the "current list" is also passed to the binary function argument -- not a major difference.

Now, in Coq we can define a list in another subtly different way:

Inductive List2 : Type -> Type :=
  | Empty2: forall A, List2 A
  | Cons2 : forall A, A -> List2 A -> List2 A
.

It looks the same type, but there is a profound difference. Here we are not defining the type List A in terms of List A. Rather, we are defining a type function List2 : Type -> Type in terms of List2. The main point of this is that the recursive references to List2 do not have to be applied to A -- the fact that above we do so is only an incident.

Anyway, let's see the type for the induction principle:

> Check List2_rect.
forall P : forall T : Type, List2 T -> Type,
   (forall A : Type, P A (Empty2 A)) ->
   (forall (A : Type) (a : A) (l : List2 A), P A l -> P A (Cons2 A a l)) ->
   forall (T : Type) (l : List2 T), P T l

Let's remove the List2 T argument from P as we did before, basically assuming P is constant on it.

forall P : forall T : Type, Type,
   (forall A : Type, P A ) ->
   (forall (A : Type) (a : A) (l : List2 A), P A -> P A) ->
   forall (T : Type) (l : List2 T), P T

Equivalently rewritten:

forall P : (Type -> Type),
   (forall A : Type, P A) ->
   (forall (A : Type), A -> List2 A -> P A -> P A) ->
   forall (T : Type), List2 T -> P T

Which roughly corresponds, in Haskell notation

(forall a, p a) ->                          -- Empty
(forall a, a -> List2 a -> p a -> p a) ->   -- Cons
List2 t -> p t

Not so bad -- the base case now has to be a polymorphic function, much as Empty in Haskell is. It makes some sense. Similarly, the inductive case must be a polymorphic function, much as Cons is. There's an extra List2 a argument, but we can ignore that, if we want.

Now, the above is still a kind of fold/cata on a regular type. What about non regular ones? I will study

data List a = Empty | Cons a (List (a,a))

which in Coq becomes:

Inductive  List3 : Type -> Type :=
  | Empty3: forall A, List3 A
  | Cons3 : forall A, A -> List3 (A * A) -> List3 A
.

with induction principle:

> Check List3_rect.
forall P : forall T : Type, List3 T -> Type,
   (forall A : Type, P A (Empty3 A)) ->
   (forall (A : Type) (a : A) (l : List3 (A * A)), P (A * A) l -> P A (Cons3 A a l)) ->
   forall (T : Type) (l : List3 T), P T l

Removing the "dependent" part:

forall P : (Type -> Type),
   (forall A : Type, P A) ->
   (forall (A : Type), A -> List3 (A * A) -> P (A * A) -> P A ) ->
   forall (T : Type), List3 T -> P T

In Haskell notation:

   (forall a. p a) ->                                      -- empty
   (forall a, a -> List3 (a, a) -> p (a, a) -> p a ) ->    -- cons
   List3 t -> p t

Aside from the additional List3 (a, a) argument, this is a kind of fold.

Finally, what about the OP type?

data List a = Empty | Cons a (List (List a))

Alas, Coq does not accept the type

Inductive  List4 : Type -> Type :=
  | Empty4: forall A, List4 A
  | Cons4 : forall A, A -> List4 (List4 A) -> List4 A
.

since the inner List4 occurrence is not in a strictly positive position. This is probably a hint that I should stop being lazy and using Coq to do the work, and start thinking about the involved F-algebras by myself... ;-)