Lists

Posted on 2017-04-23 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\) \(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\) \(\newcommand{\a}{a}\) \(\newcommand{\b}{b}\) \(\newcommand{\c}{c}\) \(\newcommand{\p}{p}\) \(\newcommand{\q}{q}\) \(\newcommand{\r}{r}\) \(\newcommand{\s}{s}\) \(\newcommand{\x}{x}\) \(\newcommand{\y}{y}\) \(\newcommand{\z}{z}\) \(\newcommand{\bool}{\mathbb{B}}\) \(\newcommand{\btrue}{\mathsf{true}}\) \(\newcommand{\bfalse}{\mathsf{false}}\) \(\newcommand{\bnot}{\mathsf{not}}\) \(\newcommand{\band}{\mathbin{\mathsf{and}}}\) \(\newcommand{\bor}{\mathbin{\mathsf{or}}}\) \(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\) \(\newcommand{\beq}{\mathsf{eq}}\) \(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\) \(\newcommand{\id}{\mathsf{id}}\) \(\newcommand{\compose}{\mathsf{compose}}\) \(\newcommand{\const}{\mathsf{const}}\) \(\newcommand{\apply}{\mathsf{apply}}\) \(\newcommand{\flip}{\mathsf{flip}}\) \(\newcommand{\flipB}{\mathsf{flip2}}\) \(\newcommand{\flipC}{\mathsf{flip3}}\) \(\newcommand{\flipD}{\mathsf{flip4}}\) \(\newcommand{\flipE}{\mathsf{flip5}}\) \(\newcommand{\clone}{\mathsf{clone}}\) \(\newcommand{\cloneC}{\mathsf{clone3}}\) \(\newcommand{\composeAonB}{\mathsf{compose1on2}}\) \(\newcommand{\composeAonC}{\mathsf{compose1on3}}\) \(\newcommand{\composeAonD}{\mathsf{compose1on4}}\) \(\newcommand{\composeBonA}{\mathsf{compose2on1}}\) \(\newcommand{\composeBonB}{\mathsf{compose2on2}}\) \(\newcommand{\composeConA}{\mathsf{compose3on1}}\) \(\newcommand{\ptrue}{\mathsf{ptrue}}\) \(\newcommand{\pfalse}{\mathsf{pfalse}}\) \(\newcommand{\pnot}{\mathsf{pnot}}\) \(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\) \(\newcommand{\por}{\mathbin{\mathsf{por}}}\) \(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\) \(\newcommand{\fst}{\mathsf{first}}\) \(\newcommand{\snd}{\mathsf{second}}\) \(\newcommand{\dup}{\mathsf{dup}}\) \(\newcommand{\tup}{\mathsf{tup}}\) \(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\) \(\newcommand{\tPair}{\mathsf{pair}_{\times}}\) \(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\) \(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\) \(\newcommand{\tupL}{\mathsf{tupL}}\) \(\newcommand{\tupR}{\mathsf{tupR}}\) \(\newcommand{\uncurry}{\mathsf{uncurry}}\) \(\newcommand{\curry}{\mathsf{curry}}\) \(\newcommand{\lft}{\mathsf{left}}\) \(\newcommand{\rgt}{\mathsf{right}}\) \(\newcommand{\either}{\mathsf{either}}\) \(\newcommand{\uSwap}{\mathsf{swap}_{+}}\) \(\newcommand{\uPair}{\mathsf{pair}_{+}}\) \(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\) \(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\) \(\newcommand{\isLft}{\mathsf{isLeft}}\) \(\newcommand{\isRgt}{\mathsf{isRight}}\) \(\newcommand{\nats}{\mathbb{N}}\) \(\newcommand{\zero}{\mathsf{0}}\) \(\newcommand{\next}{\mathsf{next}}\) \(\newcommand{\unnext}{\mathsf{unnext}}\) \(\newcommand{\iszero}{\mathsf{isZero}}\) \(\newcommand{\prev}{\mathsf{prev}}\) \(\newcommand{\natrec}{\mathsf{natrec}}\) \(\newcommand{\simprec}{\mathsf{simprec}}\) \(\newcommand{\bailrec}{\mathsf{bailrec}}\) \(\newcommand{\mutrec}{\mathsf{mutrec}}\) \(\newcommand{\dnatrec}{\mathsf{dnatrec}}\) \(\newcommand{\normrec}{\mathsf{normrec}}\) \(\newcommand{\findsmallest}{\mathsf{findsmallest}}\) \(\newcommand{\mnormrec}{\mathsf{mnormrec}}\) \(\newcommand{\nequal}{\mathsf{eq}}\) \(\newcommand{\nplus}{\mathsf{plus}}\) \(\newcommand{\ntimes}{\mathsf{times}}\) \(\newcommand{\nleq}{\mathsf{leq}}\) \(\newcommand{\ngeq}{\mathsf{geq}}\) \(\newcommand{\nminus}{\mathsf{minus}}\) \(\newcommand{\nmax}{\mathsf{max}}\) \(\newcommand{\nmin}{\mathsf{min}}\) \(\newcommand{\ndivalg}{\mathsf{divalg}}\) \(\newcommand{\nquo}{\mathsf{quo}}\) \(\newcommand{\nrem}{\mathsf{rem}}\) \(\newcommand{\ndiv}{\mathsf{div}}\) \(\newcommand{\ngcd}{\mathsf{gcd}}\) \(\newcommand{\ncoprime}{\mathsf{coprime}}\) \(\newcommand{\nlcm}{\mathsf{lcm}}\) \(\newcommand{\nmindiv}{\mathsf{mindiv}}\) \(\newcommand{\nisprime}{\mathsf{isPrime}}\) \(\newcommand{\npower}{\mathsf{power}}\) \(\newcommand{\nchoose}{\mathsf{choose}}\) \(\newcommand{\dom}{\mathsf{dom}}\) \(\newcommand{\cod}{\mathsf{cod}}\) \(\newcommand{\lists}[1]{\mathsf{List}(#1)}\) \(\newcommand{\nil}{\mathsf{nil}}\) \(\newcommand{\cons}{\mathsf{cons}}\) \(\newcommand{\uncons}{\mathsf{uncons}}\) \(\newcommand{\isnil}{\mathsf{isNil}}\) \(\newcommand{\tail}{\mathsf{tail}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\foldr}{\mathsf{foldr}}\) \(\newcommand{\foldl}{\mathsf{foldl}}\) \(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\) \(\newcommand{\unfoldN}{\mathsf{unfoldN}}\) \(\newcommand{\dfoldr}{\mathsf{dfoldr}}\) \(\newcommand{\cfoldr}{\mathsf{cfoldr}}\) \(\newcommand{\bfoldr}{\mathsf{bfoldr}}\) \(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\) \(\newcommand{\lfoldr}{\mathsf{lfoldr}}\) \(\newcommand{\snoc}{\mathsf{snoc}}\) \(\newcommand{\revcat}{\mathsf{revcat}}\) \(\newcommand{\rev}{\mathsf{rev}}\) \(\newcommand{\last}{\mathsf{last}}\) \(\newcommand{\cat}{\mathsf{cat}}\) \(\newcommand{\addlength}{\mathsf{addlength}}\) \(\newcommand{\length}{\mathsf{length}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\at}{\mathsf{at}}\) \(\newcommand{\map}{\mathsf{map}}\) \(\newcommand{\range}{\mathsf{range}}\) \(\newcommand{\zip}{\mathsf{zip}}\) \(\newcommand{\zipPad}{\mathsf{zipPad}}\) \(\newcommand{\unzip}{\mathsf{unzip}}\) \(\newcommand{\prefix}{\mathsf{prefix}}\) \(\newcommand{\suffix}{\mathsf{suffix}}\) \(\newcommand{\lcp}{\mathsf{lcp}}\) \(\newcommand{\lcs}{\mathsf{lcs}}\) \(\newcommand{\all}{\mathsf{all}}\) \(\newcommand{\any}{\mathsf{any}}\) \(\newcommand{\tails}{\mathsf{tails}}\) \(\newcommand{\inits}{\mathsf{inits}}\) \(\newcommand{\filter}{\mathsf{filter}}\) \(\newcommand{\elt}{\mathsf{elt}}\) \(\newcommand{\addcount}{\mathsf{addcount}}\) \(\newcommand{\count}{\mathsf{count}}\) \(\newcommand{\repeat}{\mathsf{repeat}}\) \(\newcommand{\sublist}{\mathsf{sublist}}\) \(\newcommand{\infix}{\mathsf{infix}}\) \(\newcommand{\select}{\mathsf{select}}\) \(\newcommand{\unique}{\mathsf{unique}}\) \(\newcommand{\delete}{\mathsf{delete}}\) \(\newcommand{\dedupeL}{\mathsf{dedupeL}}\) \(\newcommand{\dedupeR}{\mathsf{dedupeR}}\) \(\newcommand{\common}{\mathsf{common}}\) \(\newcommand{\disjoint}{\mathsf{disjoint}}\) \(\newcommand{\sublists}{\mathsf{sublists}}\) \(\newcommand{\take}{\mathsf{take}}\) \(\newcommand{\drop}{\mathsf{drop}}\) \(\newcommand{\takeBut}{\mathsf{takeBut}}\) \(\newcommand{\dropBut}{\mathsf{dropBut}}\) \(\newcommand{\takeWhile}{\mathsf{takeWhile}}\) \(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)

This page is part of a series on Arithmetic Made Difficult.

This post is literate Haskell; you can load the source into GHCi and play along.

{-# 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.

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})\).

Let \(A\) be a set. Then we have the following.

\(\uncons(\nil) = \lft(\ast)\).
\(\uncons(\cons(a,x)) = \rgt(\tup(a)(x))\).

We have \[\begin{eqnarray*} & & \lft(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \id(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-uncons-inverse-left} = & \compose(\uncons)(\either(\const(\nil),\uncurry(\cons)))(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uncons(\either(\const(\nil),\uncurry(\cons))(\lft(\ast))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \uncons(\const(\nil)(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \uncons(\nil) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \rgt(\tup(a)(x)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \id(\rgt(\tup(a)(x))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-uncons-inverse-left} = & \compose(\uncons)(\either(\const(\nil),\uncurry(\cons)))(\rgt(\tup(a)(x))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uncons(\either(\const(\nil),\uncurry(\cons))(\rgt(\tup(a)(x)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \uncons(\uncurry(\cons)(\tup(a)(x))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-uncurry} = & \uncons(\cons(a,x)) \end{eqnarray*}\] as claimed.

As a consequence, we can use \(\uncons\) to characterize equality for lists.

Let \(A\) be a set. Then we have the following.

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}\).
\(\nil\) and \(\cons(a,x)\) are not equal for any \(a\) and \(x\).
\(\cons(a,x) = \cons(b,y)\) if and only if \(a = b\) and \(x = y\).

Let \(z \in \lists{A}\). We have two possibilities for \(\uncons(z)\). If \(\uncons(z) = \lft(\ast)\), then \[\begin{eqnarray*} & & z \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \id(z) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-uncons-inverse-right} = & \compose(\either(\const(\nil),\uncurry(\cons)))(\uncons)(z) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \either(\const(\nil),\uncurry(\cons))(\uncons(z)) \\ & \hyp{\uncons(z) = \lft(\ast)} = & \either(\const(\nil),\uncurry(\cons))(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(\nil)(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \nil \end{eqnarray*}\] and if \(\uncons(z) = \rgt(a,x)\), then \[\begin{eqnarray*} & & z \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \id(z) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-uncons-inverse-right} = & \compose(\either(\const(\nil),\uncurry(\cons)))(\uncons)(z) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#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{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \uncurry(\cons)(\tup(a)(x)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-uncurry} = & \cons(a,x) \end{eqnarray*}\] as claimed.
If \(\nil = \cons(a,x)\), we have \[\begin{eqnarray*} & & \lft(\ast) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-uncons-nil} = & \uncons(\nil) \\ & \hyp{\cons(a,x) = \nil} = & \uncons(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-uncons-cons} = & \rgt(\tup(a)(x)) \end{eqnarray*}\] which is absurd.
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{/posts/arithmetic-made-difficult/Lists.html#thm-uncons-cons} = & \uncons(\cons(a,x)) \\ & \hyp{\cons(a,x) = \cons(b,y)} = & \uncons(\cons(b,y)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#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:

(\(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:

(\(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}\).

(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.

(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

\(f(\nil) \in C\).
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}\).

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.

Let \(A\) be a set. Then we have \[\foldr(\nil)(\cons)(x) = x\] for all \(x \in \lists{A}\).

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{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \cons(a,\foldr(\nil)(\cons)(x)) \\ & \hyp{\foldr(\nil)(\cons)(x) = x} = & \cons(a,x) \end{eqnarray*}\] as claimed.