<p>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:</p>

<pre><code>(* Take a coalgebra, produce a list *)
val unfold : ('a -&gt; ('b * 'a) option) -&gt; 'a -&gt; 'b list

let rec unfold f seed = 
  match f seed with 
  | None -&gt; []
  | Some(x, seed') -&gt; x :: unfold f seed'
</code></pre>

<p>Now the <code>zip</code> operation is as easy as falling off a log:</p>

<pre><code>val zip : 'a list * 'b list -&gt; ('a * 'b) list
let zip (xs, ys) = 
  let step = function
    | (x :: xs, y :: ys) -&gt; Some ((x,y), (xs, ys))
    | _ -&gt; None
  in
  unfold step (xs, ys)
</code></pre>

<p>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 <a href="https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf" rel="nofollow noreferrer"><em>Fast and Loose Reasoning is Morally Correct</em></a>, or (c) you can worry about it, and look up how to get <a href="http://www.cs.ru.nl/~venanzio/publications/Comonads_IandC.pdf" rel="nofollow noreferrer"><em>Recursive Coalgebras from Comonads</em></a>.</p>

CC BY-SA 4.0
2019-12-02T22:24:42.730Z
2019-12-02T22:24:42.730Z
Neel Krishnaswami
<p>This complication is the same as in the definition of the <a href="https://en.wikipedia.org/wiki/Church_encoding#Derivation_of_predecessor_function" rel="nofollow noreferrer">Church predecessor function</a>. 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.</p>

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

<pre><code>-- foldr :: (a -&gt; b -&gt; b) -&gt; b -&gt; [a] -&gt; b

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

zip :: [a] -&gt; [b] -&gt; [(a, b)]
zip = foldr (\a hyp ys -&gt; split ys [] (\b ys -&gt; (a, b): hyp ys))
            (\_ -&gt; [])
</code></pre>

<p>With <code>split</code> we can branch on whether a list is empty or non-empty, and we rebuild the tail of the list from the end. <code>zip</code> 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.</p>

CC BY-SA 4.0
2019-12-02T06:59:46.157Z
One purpose of point-free definitions in functional programming is to intimidate people.
Andrej Bauer
CC BY-SA 4.0
2019-12-01T12:21:41.560Z
2019-12-03T15:44:51.727Z
2019-12-03T15:44:51.727Z
András Kovács
<p>One can implement <code>zip</code> for lists, by writing specific code. However, that code is <em>ad hoc</em> and not expressed purely through the universal map (the catamorphism) from an initial algebra (<span class="math-container">$\mu F_A$</span>) to something else. All versions of the code of <code>zip</code> for lists I've seen are written via certain <em>ad hoc</em> functions that are specific for lists and are not just catamorphisms.</p>
<p>Actually, I believe it is impossible to express the <code>zip</code> operation &quot;categorically&quot;, by which you probably mean to express it purely in terms of initial algebras and universal properties (catamorphisms) for an arbitrary <span class="math-container">$F$</span>. Here are my reasons why it is impossible.</p>
<p>If it were possible, we would have a function <code>zip</code> of type <span class="math-container">$\mu F_A \times \mu F_B \to \mu F_{A\times B}$</span> that worked at once for all functors <code>F</code>. The function <code>zip</code> would be a catamorphism (the universal map) from <span class="math-container">$\mu F_A$</span>, say, to some other <span class="math-container">$F$</span>-algebra.</p>
<p>Catamorphisms work by traversing recursive data structures of type <span class="math-container">$\mu F_A$</span>. For example, if <span class="math-container">$F_A ~r = A + r\times r$</span> then the initial algebra <span class="math-container">$\mu F_A$</span>  is the type of non-empty binary trees with leaf values of type <span class="math-container">$A$</span>. A catamorphism from <span class="math-container">$\mu F_A$</span> will traverse the structure of a particular binary tree, iterating over the specific branch structure of that tree.</p>
<p>However, the <code>zip</code> operation for non-empty binary trees is a function of two trees that needs to traverse both trees; it cannot work by traversing just one of the trees. The reason is that if two trees have different branch structure then the <code>zip</code> operation must replicate both branch structures in the resulting tree. As an example, consider the following two trees:</p>
<pre><code>            .                     .
           / \                   / \
    t1 =  a   b           t2 =  c  /\
                                  /\ f
                                 d  e
</code></pre>
<p>Suppose <code>a</code> and <code>b</code> have type <span class="math-container">$A$</span> and <code>c</code>, <code>d</code>, <code>e</code>, <code>f</code> have type <span class="math-container">$B$</span>. The tree <code>zip (t1, t2)</code> must be a binary tree with leaves of type <span class="math-container">$A \times B$</span>.</p>
<p>What could be the value of <code>zip (t1, t2)</code>? Its left branch should be <code>Leaf (a, c)</code>, but what should be the right branch? We cannot leave the right branch empty, because this type of binary trees does not support empty subtrees. (A subtree must be either a leaf or a branching point with two non-empty subtrees.) The right branch cannot be just <code>Leaf b</code> because it needs to have type <span class="math-container">$A\times B$</span>. We cannot get any values of type <span class="math-container">$B$</span> without traversing the right branch of <code>t2</code>. The right branch of <code>t2</code> could be arbitrarily deep, and we won't get any values of type <code>B</code> until we traverse <code>t2</code>.</p>
<p>The only law-abiding implementation of <code>zip</code> must give the following result for <code>zip (t1, t2)</code>:</p>
<pre><code>                      .
                     / \
                    /   \
                   /     .
 zip (t1, t2) =  (a, c) / \  
                       / \ (b, f)
                      /   \
                  (b, d) (b, e)
</code></pre>
<p>This consideration shows that one cannot compute <code>zip (t1, t2)</code> without traversing both <code>t1</code> and <code>t2</code>.</p>
<p>This situation is different from the standard <code>zip</code> operation for lists, where the result is truncated at the smallest length among the two lists. But we cannot truncate the non-empty binary tree.</p>
<p>At least, this consideration shows that implementing <code>zip</code> for arbitrary fixpoint types <span class="math-container">$\mu F_A$</span> is not possible without further assumptions on <span class="math-container">$F$</span>.  For some <span class="math-container">$F$</span>, the data structure type <span class="math-container">$\mu F_A$</span> will support truncation, for other <span class="math-container">$F$</span> it will not. The <code>zip</code> operation will have to be implemented differently in each case.</p>
<p>So, one cannot implement <code>zip</code> of type <span class="math-container">$\mu F_A \times \mu F_B \to \mu F_{A\times B}$</span> via code that works in the same way for all <span class="math-container">$F$</span>.</p>
<p>This shows the impossibility of expressing <code>zip</code> purely via universal properties of the initial <span class="math-container">$F$</span>-algebras.</p>

CC BY-SA 4.0
2024-10-24T18:48:38.467Z
2024-10-25T07:16:21.867Z
2024-10-25T07:16:21.867Z
winitzki
<h2>Lists and fixpoints</h2>

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

<pre><code>data List a
   = Nil
   | Cons a (List a)
</code></pre>

<p>Here, <code>Nil</code> is the sole inhabitant of <span class="math-container">$1$</span>, and <code>Cons a as</code> corresponds to <code>A \times X</code>. The fact that lists are fixpoints is reflected in the recursive definition of <code>List a</code>.</p>

<h2>Initial algebras</h2>

<p>It is well known that least fixpoints have semantics in initial algebras.
See e.g. <a href="https://www.csc.depauw.edu/~bhoward/papers/" rel="noreferrer">Brian Howard's thesis</a>. For our purposes, the type of <span class="math-container">$A$</span>-lists is the initial algebra of the functor <span class="math-container">$F_A$</span>.</p>

<h3>Algebra map</h3>

<p>Being an algebra, lists come with the algebra map <span class="math-container">$\phi\colon F_A (\mu F_A) \to \mu F_A$</span>. It an isomorphism, so if we unpack we have <span class="math-container">$1 + A \times \mu F_A \cong \mu F_A$</span>. In words, a list is either empty or consists of an <span class="math-container">$A$</span> and another list.</p>

<h3>Universal property</h3>

<p>Since <span class="math-container">$\mu F_A$</span> is <em>initial</em>, there is a unique algebra map from <span class="math-container">$A$</span>-lists to any <span class="math-container">$F_A$</span> algebra. That is, if there is a morphism <span class="math-container">$\beta\colon F_A B \to B$</span>, there is a unique algebra map <span class="math-container">$\mathrm{it}(\beta)\colon \mu F_A \to B$</span>.</p>

<h2>Warm up: Unzip</h2>

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

<p><span class="math-container">$$F_{A \times B} (\mu F_A \times \mu F_B) = 1 + A \times B \times  \mu F_A \times \mu F_B$$</span>
<span class="math-container">$$\hookrightarrow 1 + A \times \mu F_A + B \times \mu F_B + A \times B \times \mu F_A \times \mu F_B$$</span>
<span class="math-container">$$\cong (1 + A \times \mu F_A) \times (1 + B \times \mu F_B) = \mu F_A \times \mu F_B$$</span></p>

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

<h2>Puzzle: Zip</h2>

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

<pre><code>zip (Cons a as) (Cons b bs) = Cons (a, b) $ zip as bs
zip _ _ = Nil
</code></pre>

<p>But now we need to write a function <em>into</em> 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 <span class="math-container">$\mu F_{A \times B}$</span> for some other functor, but I don't know which, and I don't know how to map from <em>two</em> fixpoints into a single one.</p>

CC BY-SA 4.0
2019-12-01T10:14:49.790Z
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
CC BY-SA 4.0
2019-12-01T10:35:22.460Z
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
CC BY-SA 4.0
2019-12-01T15:56:38.497Z
@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
CC BY-SA 4.0
2019-12-02T06:58:44.210Z
Aha, that's a reasonable option as well.
Andrej Bauer
<type-theory><inductive-type>
How to define list zipping categorically/inductively?
Turion
# How to define list zipping categorically/inductively?

(Asked by: username_0 on 2019-11-30)

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.

**Tags:** type-theory, inductive-type
> **Comments:**
> **username_1**: 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?  
> **username_1**: 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))`.  
> **username_0**: @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 ```  
> **username_1**: Aha, that's a reasonable option as well.  

---

## 3 answers

### Answer by username_2 on 2019-12-02. Score: 2 | Accepted answer

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.


---

### Answer by username_3 on 2019-12-01. Score: 5

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.

> **Comments:**
> **username_1**: One purpose of point-free definitions in functional programming is to intimidate people.  

---

### Answer by username_4 on 2024-10-24. Score: 2

One can implement zip for lists, by writing specific code. However, that code is ad hoc and not expressed purely through the universal map (the catamorphism) from an initial algebra ($\mu F_A$) to something else. All versions of the code of zip for lists I've seen are written via certain ad hoc functions that are specific for lists and are not just catamorphisms.
Actually, I believe it is impossible to express the zip operation "categorically", by which you probably mean to express it purely in terms of initial algebras and universal properties (catamorphisms) for an arbitrary $F$. Here are my reasons why it is impossible.
If it were possible, we would have a function zip of type $\mu F_A \times \mu F_B \to \mu F_{A\times B}$ that worked at once for all functors F. The function zip would be a catamorphism (the universal map) from $\mu F_A$, say, to some other $F$-algebra.
Catamorphisms work by traversing recursive data structures of type $\mu F_A$. For example, if $F_A ~r = A + r\times r$ then the initial algebra $\mu F_A$  is the type of non-empty binary trees with leaf values of type $A$. A catamorphism from $\mu F_A$ will traverse the structure of a particular binary tree, iterating over the specific branch structure of that tree.
However, the zip operation for non-empty binary trees is a function of two trees that needs to traverse both trees; it cannot work by traversing just one of the trees. The reason is that if two trees have different branch structure then the zip operation must replicate both branch structures in the resulting tree. As an example, consider the following two trees:
            .                     .
           / \                   / \
    t1 =  a   b           t2 =  c  /\
                                  /\ f
                                 d  e

Suppose a and b have type $A$ and c, d, e, f have type $B$. The tree zip (t1, t2) must be a binary tree with leaves of type $A \times B$.
What could be the value of zip (t1, t2)? Its left branch should be Leaf (a, c), but what should be the right branch? We cannot leave the right branch empty, because this type of binary trees does not support empty subtrees. (A subtree must be either a leaf or a branching point with two non-empty subtrees.) The right branch cannot be just Leaf b because it needs to have type $A\times B$. We cannot get any values of type $B$ without traversing the right branch of t2. The right branch of t2 could be arbitrarily deep, and we won't get any values of type B until we traverse t2.
The only law-abiding implementation of zip must give the following result for zip (t1, t2):
                      .
                     / \
                    /   \
                   /     .
 zip (t1, t2) =  (a, c) / \  
                       / \ (b, f)
                      /   \
                  (b, d) (b, e)

This consideration shows that one cannot compute zip (t1, t2) without traversing both t1 and t2.
This situation is different from the standard zip operation for lists, where the result is truncated at the smallest length among the two lists. But we cannot truncate the non-empty binary tree.
At least, this consideration shows that implementing zip for arbitrary fixpoint types $\mu F_A$ is not possible without further assumptions on $F$.  For some $F$, the data structure type $\mu F_A$ will support truncation, for other $F$ it will not. The zip operation will have to be implemented differently in each case.
So, one cannot implement zip of type $\mu F_A \times \mu F_B \to \mu F_{A\times B}$ via code that works in the same way for all $F$.
This shows the impossibility of expressing zip purely via universal properties of the initial $F$-algebras.


---

