# How to define list zipping categorically/inductively?

## Lists and fixpoints

The type of $$A$$-lists is defined as $$\mu F_A$$, where $$F_A(X) = 1 + A \times X$$ is the "cons-or-nil"-functor and $$\mu$$ is the least fixpoint operator. In Haskell syntax, this would correspond to:

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


Here, Nil is the sole inhabitant of $$1$$, and Cons a as corresponds to A \times X. The fact that lists are fixpoints is reflected in the recursive definition of List a.

## Initial algebras

It is well known that least fixpoints have semantics in initial algebras. See e.g. Brian Howard's thesis. For our purposes, the type of $$A$$-lists is the initial algebra of the functor $$F_A$$.

### Algebra map

Being an algebra, lists come with the algebra map $$\phi\colon F_A (\mu F_A) \to \mu F_A$$. It an isomorphism, so if we unpack we have $$1 + A \times \mu F_A \cong \mu F_A$$. In words, a list is either empty or consists of an $$A$$ and another list.

### Universal property

Since $$\mu F_A$$ is initial, there is a unique algebra map from $$A$$-lists to any $$F_A$$ algebra. That is, if there is a morphism $$\beta\colon F_A B \to B$$, there is a unique algebra map $$\mathrm{it}(\beta)\colon \mu F_A \to B$$.

## Warm up: Unzip

unzip takes a list of pairs $$\mu F_{A \times B}$$ and produces a pair of lists $$\mu F_A \times \mu F_B$$. It is thus a function from a list into something else, and could thus be defined via the universal property. All we need to do is to give $$\mu F_A \times \mu F_B$$ the right $$F_{A \times B}$$-structure:

$$F_{A \times B} (\mu F_A \times \mu F_B) = 1 + A \times B \times \mu F_A \times \mu F_B$$ $$\hookrightarrow 1 + A \times \mu F_A + B \times \mu F_B + A \times B \times \mu F_A \times \mu F_B$$ $$\cong (1 + A \times \mu F_A) \times (1 + B \times \mu F_B) = \mu F_A \times \mu F_B$$

One can see that we inject into either the case "both lists stop" or "both lists continue". Apply the universal property, and you have unzip.

## Puzzle: Zip

Now we would like to do the reverse. Given two lists, create a list of pairs. The Haskell version is simple:

zip (Cons a as) (Cons b bs) = Cons (a, b) $zip as bs zip _ _ = Nil  But now we need to write a function into a list. This suggests using the algebra morphism, but I can't figure out how. Alternatively, one might want to create an algebra structure for $$\mu F_{A \times B}$$ for some other functor, but I don't know which, and I don't know how to map from two fixpoints into a single one. • You need to specify what happens if you're zipping lists of different lengths. In Haskell you'll get an error, but in category theory you need to be explicit about it. So, what should the result be? – Andrej Bauer Dec 1 '19 at 10:14 • What I am saying is that you should have zip : List a -> List b -> Maybe (List (a, b)). You can define zip using initiality of List a to get a morphism into List b -> Maybe (List (a, b)). – Andrej Bauer Dec 1 '19 at 10:35 • @AndrejBauer I think the way I wrote it, zip as bs will not be an error if as and bs are different length, but the list will end if either as or bs ends. The catch-all pattern expands to:  zip (Cons a as) (Cons b bs) = Cons (a, b)$ zip as bs zip (Cons _ _) Nil = Nil zip Nil (Cons _ _) = Nil zip Nil Nil = Nil  – Turion Dec 1 '19 at 15:56
• Aha, that's a reasonable option as well. – Andrej Bauer Dec 2 '19 at 6:58

This complication is the same as in the definition of the Church predecessor function. We need to take the tail of a list, but we only have a folding operation given by (weak) initiality, which does not directly provide access to that, so we need to rebuild the tail from the right end.

It is the easiest to write the solution in a lambda calculus with products, exponentials and foldr for lists, witnessing weak initiality. In Haskell:

-- foldr :: (a -> b -> b) -> b -> [a] -> b

-- matching on whether a list is empty or non-empty
split :: [a] -> b -> (a -> [a] -> b) -> b
split as b f = fst (foldr (\a (b, as) -> (f a as, a:as)) (b, []) as)

zip :: [a] -> [b] -> [(a, b)]
zip = foldr (\a hyp ys -> split ys [] (\b ys -> (a, b): hyp ys))
(\_ -> [])


With split we can branch on whether a list is empty or non-empty, and we rebuild the tail of the list from the end. zip can be translated back to cartesian closed categories with list objects, but of course a precise definition in that setting would be much less readable, because of the mandatory point-free definitions.

• One purpose of point-free definitions in functional programming is to intimidate people. – Andrej Bauer Dec 2 '19 at 6:59

The right (i.e., my personally preferred) way to think about this is in terms of unfolds, rather than folds. So first define the unfold:

(* Take a coalgebra, produce a list *)
val unfold : ('a -> ('b * 'a) option) -> 'a -> 'b list

let rec unfold f seed =
match f seed with
| None -> []
| Some(x, seed') -> x :: unfold f seed'


Now the zip operation is as easy as falling off a log:

val zip : 'a list * 'b list -> ('a * 'b) list
let zip (xs, ys) =
let step = function
| (x :: xs, y :: ys) -> Some ((x,y), (xs, ys))
| _ -> None
in
unfold step (xs, ys)


Now, it may bother you that lists are inductive, and unfolds are coinductive. If so, you can either (a) not worry about it because inductive and coinductive types coincide in lazy languages like Haskell, (b) not worry about it, since Fast and Loose Reasoning is Morally Correct, or (c) you can worry about it, and look up how to get Recursive Coalgebras from Comonads.