---
title: Lists
author: nbloomf
date: 2017-04-23
tags: arithmetic-made-difficult, literate-haskell
slug: lists
---
> {-# LANGUAGE NoImplicitPrelude, ScopedTypeVariables #-}
> module Lists
> ( List(..), ConsList(), foldr
> ) where
>
> import Testing
> import Booleans
> import And
> import Tuples
> import DisjointUnions
In the previous post, we saw how the process of describing $\nats$ in terms of its universal map $\natrec$ can be generalized: take an endofunctor $F$, assume it has an initial algebra, and see how it behaves. Here's an example.
:::::: definition ::
Let $A$ be a set, and define a functor $F_A$ by $F_A(X) = 1 + A \times X$. We assume that $F_A$ has an initial algebra, which we will denote $\lists{A}$. We denote the component maps of the isomorphism $$\theta : 1 + A \times \lists{A} \rightarrow \lists{A}$$ by $\const(\nil) : 1 \rightarrow \lists{A}$ and $\cons : A \times \lists{A} \rightarrow \lists{A}$. That is, $$\theta = \either(\const(\nil),\cons).$$
::::::::::::::::::::
The names *nil* and *cons* come from the Lisp programming language, where they were first introduced. Now because the algebra map $\nil + \cons$ is an isomorphism, it has an inverse; we'll denote this map $\uncons : \lists{A} \rightarrow 1 + (A \times \lists{A})$.
:::::: theorem :::::
[]{#thm-uncons-inverse-left}[]{#thm-uncons-inverse-right}[]{#thm-uncons-nil}[]{#thm-uncons-cons}
Let $A$ be a set. Then we have the following.
1. $\uncons(\nil) = \lft(\ast)$.
2. $\uncons(\cons(a,x)) = \rgt(\tup(a)(x))$.
::: proof ::::::::::
1. We have
$$\begin{eqnarray*}
& & \lft(\ast) \\
& \href{@functions@#def-id}
= & \id(\lft(\ast)) \\
& \href{@lists@#def-uncons-inverse-left}
= & \compose(\uncons)(\either(\const(\nil),\uncurry(\cons)))(\lft(\ast)) \\
& \href{@functions@#def-compose}
= & \uncons(\either(\const(\nil),\uncurry(\cons))(\lft(\ast))) \\
& \href{@disjoint-unions@#def-either-lft}
= & \uncons(\const(\nil)(\ast)) \\
& \href{@functions@#def-const}
= & \uncons(\nil)
\end{eqnarray*}$$
as claimed.
2. We have
$$\begin{eqnarray*}
& & \rgt(\tup(a)(x)) \\
& \href{@functions@#def-id}
= & \id(\rgt(\tup(a)(x))) \\
& \href{@lists@#def-uncons-inverse-left}
= & \compose(\uncons)(\either(\const(\nil),\uncurry(\cons)))(\rgt(\tup(a)(x))) \\
& \href{@functions@#def-compose}
= & \uncons(\either(\const(\nil),\uncurry(\cons))(\rgt(\tup(a)(x)))) \\
& \href{@disjoint-unions@#def-either-rgt}
= & \uncons(\uncurry(\cons)(\tup(a)(x))) \\
& \href{@tuples@#def-uncurry}
= & \uncons(\cons(a,x))
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::
::::::::::::::::::::
As a consequence, we can use $\uncons$ to characterize equality for lists.
:::::: theorem :::::
[]{#thm-list-eq-nil}[]{#thm-list-eq-cons}
Let $A$ be a set. Then we have the following.
1. Every element of $\lists{A}$ is equal to either $\nil$ or to $\cons(a,x)$ for some $a \in A$ and $x \in \lists{A}$.
2. $\nil$ and $\cons(a,x)$ are not equal for any $a$ and $x$.
3. $\cons(a,x) = \cons(b,y)$ if and only if $a = b$ and $x = y$.
::: proof ::::::::::
1. Let $z \in \lists{A}$. We have two possibilities for $\uncons(z)$. If $\uncons(z) = \lft(\ast)$, then
$$\begin{eqnarray*}
& & z \\
& \href{@functions@#def-id}
= & \id(z) \\
& \href{@lists@#def-uncons-inverse-right}
= & \compose(\either(\const(\nil),\uncurry(\cons)))(\uncons)(z) \\
& \href{@functions@#def-compose}
= & \either(\const(\nil),\uncurry(\cons))(\uncons(z)) \\
& \hyp{\uncons(z) = \lft(\ast)}
= & \either(\const(\nil),\uncurry(\cons))(\lft(\ast)) \\
& \href{@disjoint-unions@#def-either-lft}
= & \const(\nil)(\ast) \\
& \href{@functions@#def-const}
= & \nil
\end{eqnarray*}$$
and if $\uncons(z) = \rgt(a,x)$, then
$$\begin{eqnarray*}
& & z \\
& \href{@functions@#def-id}
= & \id(z) \\
& \href{@lists@#def-uncons-inverse-right}
= & \compose(\either(\const(\nil),\uncurry(\cons)))(\uncons)(z) \\
& \href{@functions@#def-compose}
= & \either(\const(\nil),\uncurry(\cons))(\uncons(z)) \\
& \hyp{\uncons(z) = \rgt(\tup(a)(x))}
= & \either(\const(\nil),\uncurry(\cons))(\rgt(\tup(a)(x))) \\
& \href{@disjoint-unions@#def-either-rgt}
= & \uncurry(\cons)(\tup(a)(x)) \\
& \href{@tuples@#def-uncurry}
= & \cons(a,x)
\end{eqnarray*}$$
as claimed.
2. If $\nil = \cons(a,x)$, we have
$$\begin{eqnarray*}
& & \lft(\ast) \\
& \href{@lists@#thm-uncons-nil}
= & \uncons(\nil) \\
& \hyp{\cons(a,x) = \nil}
= & \uncons(\cons(a,x)) \\
& \href{@lists@#thm-uncons-cons}
= & \rgt(\tup(a)(x))
\end{eqnarray*}$$
which is absurd.
3. The "if" direction is clear. To see the "only if" direction, suppose $\cons(a,x) = \cons(b,y)$. Then we have
$$\begin{eqnarray*}
& & \rgt(\tup(a)(x)) \\
& \href{@lists@#thm-uncons-cons}
= & \uncons(\cons(a,x)) \\
& \hyp{\cons(a,x) = \cons(b,y)}
= & \uncons(\cons(b,y)) \\
& \href{@lists@#thm-uncons-cons}
= & \rgt(\tup(b)(y))
\end{eqnarray*}$$
so that $(a,x) = (b,y)$, and thus $a = b$ and $x = y$ as claimed.
::::::::::::::::::::
::::::::::::::::::::
So what do the elements of $\lists{A}$ look like? Well, applying our "constructor" functions we can build elements like
$$\begin{array}{c}
\nil \\
\cons(a,\nil) \\
\cons(b,\cons(a,\nil)) \\
\cons(c,\cons(b,\cons(a,\nil))) \\
\vdots
\end{array}$$
We will wrap this definition up in code both as a concrete type and as a type class, so that later we can give alternative implementations. The list algebra is characterized by the components of the algebra map ($\nil$ and $\cons$) as well as the inverse map ($\uncons$).
> class List t where
> nil :: t a
>
> cons :: a -> t a -> t a
>
> uncons :: t a -> Union () (Pair a (t a))
>
> list :: [a] -> t a
And the concrete type:
> data ConsList a = N | C a (ConsList a)
> deriving Show
>
>
> instance List ConsList where
> nil = N
>
> cons = C
>
> uncons m = case m of
> N -> lft ()
> C a x -> rgt (tup a x)
>
> list m = case m of
> [] -> N
> (x:xs) -> C x (list xs)
>
>
> instance (Equal a) => Equal (ConsList a) where
> eq N N = true
> eq N (C _ _) = false
> eq (C _ _) N = false
> eq (C a x) (C b y) = and (eq a b) (eq x y)
>
>
> instance (TypeName a) => TypeName (ConsList a) where
> typeName _ = "ConsList " ++ (typeName (undefined :: a))
>
>
> instance (Arbitrary a) => Arbitrary (ConsList a) where
> arbitrary = do
> xs <- arbitrary
> return (list xs)
>
> shrink N = []
> shrink (C _ x) = [x]
>
>
> instance (Arbitrary a) => CoArbitrary (ConsList a) where
> coarbitrary N = variant (0 :: Integer)
> coarbitrary (C _ x) = variant (1 :: Integer) . coarbitrary x
This business about initial algebras is nice, but it will be convenient to unpack this definition a little bit. First, we give the following more concrete description of $F_A$-algebras:
:::::: definition ::
($A$-inductive set.) Let $A$ be a set. An $A$-inductive set is a set $B$ together with an element $e$ and a mapping $f : A \times B \rightarrow B$.
::::::::::::::::::::
And a more concrete decription of $F_A$-algebra morphisms:
:::::: definition ::
($A$-inductive set homomorphism.) Let $A$ be a set. Given two $A$-inductive sets $(B,e,f)$ and $(C,u,g)$, an $A$-inductive set homomorphism is a mapping $\varphi : B \rightarrow C$ such that $\varphi(e) = u$ and $$\varphi(f(a,x)) = g(a,\varphi(x))$$ for all $a \in A$ and $x \in B$.
::::::::::::::::::::
And finally, a more concrete description of the universal algebra from $\lists{A}$.
:::::: axiom :::::::
[]{#def-foldr-nil}[]{#def-foldr-cons}
(Fold.) Let $A$ be a set, and let $(B,e,\varphi)$ be an $A$-inductive set. Then there is a unique map $\Theta : \lists{A} \rightarrow B$ which solves the system of functional equations $$\left\{ \begin{array}{l} \Theta(\nil) = e \\ \Theta(\cons(a,x)) = \varphi(a,\Theta(x)). \end{array} \right.$$ We denote this unique $\Theta$ by $\foldr(e)(\varphi)$.
In Haskell:
> foldr :: (List t) => b -> (a -> b -> b) -> t a -> b
> foldr e phi x = case uncons x of
> Left () -> e
> Right (Pair a as) -> phi a (foldr e phi as)
::::::::::::::::::::
Note that this definition is *not* tail recursive. This turns out not to be a huge problem in practice.
It's handy to remember that this theorem says not only that $\foldr(\ast)(\ast)$ exists, but that it is unique -- in some sense foldr gives the unique solution to a system of functional equations. This gives us a strategy for showing that two programs are equivalent. If one is defined as a fold, and both programs satisfy the universal property, then they have to be equal. This is nice for showing, for instance, that a *slow but obviously correct* program is equivalent to a *fast but not obviously correct* one.
Now $\lists{A}$ has an inductive proof strategy.
:::::: theorem :::::
(List Induction.) Let $A$ be a set, and let $f : \lists{A} \rightarrow B$ be a map. Suppose $C \subseteq B$ is a subset with the property that
1. $f(\nil) \in C$.
2. If $f(x) \in C$ and $a \in A$, then $f(\cons(a,x)) \in C$.
Then we have $f(x) \in C$ for all $x \in \lists{A}$.
::: proof ::::::::::
This proof is analogous to the proof of the induction principle for $\nats$. We first define $T \subseteq \lists{A}$ by $$T = \{x \in \lists{A} \mid f(x) \in C \}.$$ Note that $\nil \in T$ and if $x \in T$ and $a \in A$ then $\cons(a,x) \in T$; in particular, $(T,\nil,\cons)$ is an $A$-iterative set. We let $\Theta = \foldr(\nil)(\cons)$. Now the inclusion map $\iota : T \rightarrow \lists{A}$ is an $A$-inducive set homomorphism, since $\iota(\nil) = \nil$ and $$\iota(\cons(a,x)) = \cons(a,x) = \cons(a,\iota(x)).$$ Thus $\iota \circ \Theta : \lists{A} \rightarrow \lists{A}$ is an $A$-inductive set homomorphism, so it must be $\id_A$. Thus if $x \in \lists{A}$ we have $$x = \id(x) = \iota(\Theta(x)) = \Theta(x) \in T$$ so that $f(x) \in C$ as claimed.
::::::::::::::::::::
::::::::::::::::::::
Here's an example using list induction.
:::::: theorem :::::
[]{#thm-foldr-nil-cons}
Let $A$ be a set. Then we have $$\foldr(\nil)(\cons)(x) = x$$ for all $x \in \lists{A}$.
::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, we have $$\foldr(\nil)(\cons)(\nil) = \nil$$ as claimed. For the inductive step, suppose the equality holds for some $x \in \lists{A}$, and let $a \in A$. Now
$$\begin{eqnarray*}
& & \foldr(\nil)(\cons)(\cons(a,x)) \\
& \href{@lists@#def-foldr-cons}
= & \cons(a,\foldr(\nil)(\cons)(x)) \\
& \hyp{\foldr(\nil)(\cons)(x) = x}
= & \cons(a,x)
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::
::::::::::::::::::::