Length

Posted on 2017-04-26 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 #-}
module Length
  ( addlength, length, _test_length, main_length
  ) where

import Testing
import Functions
import Flip
import NaturalNumbers
import Plus
import Lists
import LeftFold
import Snoc
import Reverse
import Cat

Today we’ll measure the sizes of lists with $\length$ . Intuitively this function should “count” the “number” of “items” in a list. Thinking recursively, it is reasonable to want the length of $\nil$ to be zero, and the length of $\cons(a,x)$ to be one more than the length of $x$ . $\foldr(\ast)(\ast)$ was made for situations like this. But wait! Remember that $\foldr(\ast)(\ast)$ is not tail recursive, so on large lists it may have problems. But $\foldl(\ast)$ is tail recursive, and is interchangeable with $\foldr(\ast)(\ast)$ as long as whatever we’re doing to the list doesn’t care what order the items come in. And it seems reasonable to say that the length of a list is not dependent on the order of its items. So we’ll use $\foldl(\ast)$ . Recall from $\rev$ that $\foldl(\ast)$ is easier to reason about if it remains parameterized on the “base case”. With that in mind, we start with a helper function $\addlength$ .

Let $A$ be a set. We define $\addlength : \nats \rightarrow \lists{A} \rightarrow \nats$ by $\addlength = \foldl(\compose(\const)(\next))$ .

In Haskell:

addlength :: (List t, Natural n) => n -> t a -> n
addlength = foldl (compose const next)

Since $\addlength$ is defined as a $\foldl(\ast)$ , it is the unique solution to a system of functional equations.

Let $A$ be a set. Then $\addlength$ is the unique map $f : \nats \times \lists{A} \rightarrow \nats$ such that for all $n \in \nats$ , $a \in A$ , and $x \in \lists{A}$ , we have $\left\{\begin{array}{l} f(n,\nil) = n \\ f(n,\cons(a,x)) = f(\next(n),x) \end{array}\right.$

_test_addlength_nil_right
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (n -> Bool)
_test_addlength_nil_right t _ =
  testName "addlength(n,nil) == n" $
  \n ->
    let nil' = nil `withTypeOf` t in
    eq (addlength n nil') n


_test_addlength_cons_right
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (n -> a -> t a -> Bool)
_test_addlength_cons_right _ _ =
  testName "addlength(n,cons(a,x)) == addlength(next(n),x)" $
  \n a x ->
    eq (addlength n (cons a x)) (addlength (next n) x)

$\addlength$ interacts with $\cons$ and $\snoc$ .

Let $A$ be a set. For all $n \in \nats$ , $a \in A$ , and $x \in \lists{A}$ , we have the following.

$\addlength(n,\snoc(a,x)) = \next(\addlength(n,x))$ .
$\addlength(n,\cons(a,x)) = \next(\addlength(n,x))$ .

We have $\begin{eqnarray*} & & \addlength(n,\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#def-addlength} = & \foldl(\compose(\const)(\next))(n,\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-snoc-foldl} = & \compose(\const)(\next)(\foldl(\compose(\const)(\next))(n,x),a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \const(\next(\foldl(\compose(\const)(\next))(n,x)))(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \next(\foldl(\compose(\const)(\next))(n,x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#def-addlength} = & \next(\addlength(n,x)) \end{eqnarray*}$ as claimed.
We proceed by list induction on $x$ . For the base case $x = \nil$ , we have $\begin{eqnarray*} & & \addlength(n,\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-addlength-cons} = & \addlength(\next(n),\nil) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-addlength-nil} = & \next(n) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-addlength-nil} = & \next(\addlength(n,\nil)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $a$ and $n$ for some $x$ , and let $b \in A$ . Now $\begin{eqnarray*} & & \addlength(n,\cons(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-addlength-cons} = & \addlength(\next(n),\cons(b,x)) \\ & \hyp{\addlength(k,\cons(b,x)) = \next(\addlength(k,x))} = & \next(\addlength(\next(n),x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-addlength-cons} = & \next(\addlength(n,\cons(b,x))) \end{eqnarray*}$ as needed.

_test_addlength_snoc_next
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (n -> a -> t a -> Bool)
_test_addlength_snoc_next _ _ =
  testName "addlength(n,snoc(a,x)) == next(addlength(n,x))" $
  \n a x ->
    eq (addlength n (snoc a x)) (next (addlength n x))


_test_addlength_cons_next
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (n -> a -> t a -> Bool)
_test_addlength_cons_next _ _ =
  testName "addlength(n,cons(a,x)) == next(addlength(n,x))" $
  \n a x ->
    eq (addlength n (cons a x)) (next (addlength n x))

$\addlength$ interacts with $\rev$ .

Let $A$ be a set. For all $n \in \nats$ and $x \in \lists{A}$ , we have $\addlength(n,\rev(x)) = \addlength(n,x).$

We proceed by list induction on $x$ . For the base case $x = \nil$ , we have $\begin{eqnarray*} & & \addlength(n,\rev(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \addlength(n,\nil) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $n$ for some $x$ , and let $a \in A$ . Now $\begin{eqnarray*} & & \addlength(n,\rev(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \addlength(n,\snoc(a,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-addlength-snoc-next} = & \next(\addlength(n,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-addlength-rev} = & \next(\addlength(n,x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-addlength-cons-next} = & \addlength(n,\cons(a,x)) \end{eqnarray*}$ as needed.

_test_addlength_rev
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (n -> t a -> Bool)
_test_addlength_rev _ _ =
  testName "addlength(n,rev(x)) == addlength(n,x)" $
  \n x ->
    eq (addlength n (rev x)) (addlength n x)

Now we define $\length$ as follows.

Let $A$ be a set. Define $\length : \lists{A} \rightarrow \nats$ by $\length(x) = \addlength(\zero,x).$

In Haskell:

length :: (List t, Natural n) => t a -> n
length = addlength zero

Although $\length$ is essentially defined as a left fold, it can be characterized as a right fold.

Let $A$ be a set. Then we have $\length(x) = \foldr(\zero)(\flip(\compose(\const)(\next)))(x).$

We proceed by list induction on $x$ . For the base case $x = \nil$ , we have $\begin{eqnarray*} & & \foldr(\zero)(\flip(\compose(\const)(\next)))(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \zero \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-addlength-nil} = & \addlength(\zero,\nil) \\ & \href{/posts/arithmetic-made-difficult/Length.html#def-length} = & \length(\nil) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$ . Now $\begin{eqnarray*} & & \foldr(\zero)(\flip(\compose(\const)(\next)))(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \flip(\compose(\const)(\next))(a,\foldr(\zero)(\flip(\compose(\const)(\next)))(x)) \\ & \hyp{\length = \foldr(\zero)(\flip(\compose(\const)(\next)))} = & \flip(\compose(\const)(\next))(a,\length(x)) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & \compose(\const)(\next)(\length(x),a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \const(\next(\length(x)))(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \next(\length(x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#def-length} = & \next(\addlength(\zero,x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-addlength-cons-next} = & \addlength(\zero,\cons(a,x)) \end{eqnarray*}$ as needed.

_test_length_foldr
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> Bool)
_test_length_foldr _ k =
  testName "length(x) == foldr(zero,flip(compose(const)(next)))(x)" $
  \x -> eq
    (length x)
    (foldr
      (zero `withTypeOf` k)
      (flip (compose const next)) x)

Since $\length$ is equivalent to a right fold, it is the unique solution to a system of functional equations.

Let $A$ be a set. $\length$ is the unique solution $f : \lists{A} \rightarrow \nats$ to the following system of equations for all $a \in A$ and $x \in \lists{A}$ . $\left\{\begin{array}{l} f(\nil) = \zero \\ f(\cons(a,x)) = \next(f(x)) \end{array}\right.$

_test_length_nil
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test Bool
_test_length_nil t k =
  testName "length(nil) == zero" $
    eq (length (nil `withTypeOf` t)) (zero `withTypeOf` k)


_test_length_cons
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> Bool)
_test_length_cons _ k =
  testName "length(cons(a,x)) == next(length(x))" $
  \a x -> eq
    ((length (cons a x)) `withTypeOf` k)
    (next (length x))

Special cases.

For all $a,b \in A$ , we have:

$\length(\cons(a,\nil)) = \next(\zero)$ .
$\length(\cons(a,\cons(b,\nil))) = \next(\next(\zero))$ .

We have $\begin{eqnarray*} & & \length(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \next(\length(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \next(\zero) \end{eqnarray*}$ as claimed.
Note that $\begin{eqnarray*} & & \length(\cons(a,\cons(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \next(\length(\cons(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-singleton} = & \next(\next(\zero)) \end{eqnarray*}$ as claimed.

_test_length_single
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> Bool)
_test_length_single t k =
  testName "length(cons(a,nil)) == next(zero)" $
  \a -> eq
    ((next zero) `withTypeOf` k)
    (length (cons a (nil `withTypeOf` t)))


_test_length_double
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> a -> Bool)
_test_length_double t k =
  testName "length(cons(a,cons(b,nil))) == next(next(zero))" $
  \a b -> eq
    ((next (next zero)) `withTypeOf` k)
    (length (cons a (cons b (nil `withTypeOf` t))))

$\length$ interacts with $\snoc$ .

For all $a \in A$ and $x \in \lists{A}$ , we have $\length(\snoc(a,x)) = \next(\length(x)).$

We have $\begin{eqnarray*} & & \length(\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#def-length} = & \addlength(\zero,\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-addlength-snoc-next} = & \next(\addlength(\zero,x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#def-length} = & \next(\length(x)) \end{eqnarray*}$ as claimed.

_test_length_snoc :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> Bool)
_test_length_snoc _ k =
  testName "length(snoc(a,x)) == next(length(x))" $
  \a x -> eq
    ((length (snoc a x)) `withTypeOf` k)
    (next (length x))

$\length$ is invariant over $\rev$ .

Let $A$ be a set. For all $x \in \lists{A}$ we have $\length(\rev(x)) = \length(x).$

Note that $\begin{eqnarray*} & & \length(\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#def-length} = & \addlength(\zero,\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-addlength-rev} = & \addlength(\zero,x) \\ & \href{/posts/arithmetic-made-difficult/Length.html#def-length} = & \length(x) \end{eqnarray*}$ as claimed.

_test_length_rev
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> Bool)
_test_length_rev _ k =
  testName "length(rev(x)) == length(x)" $
  \x -> eq
    ((length (rev x)) `withTypeOf` k)
    (length x)

$\length$ turns $\cat$ into $\nplus$ .

Let $A$ be a set. For all $x,y \in \lists{A}$ we have $\length(\cat(x,y)) = \nplus(\length(x),\length(y)).$

We proceed by list induction on $y$ . For the base case $y = \nil$ , note that $\begin{eqnarray*} & & \length(\cat(x,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & \length(x) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-zero-right} = & \nplus(\length(x),\zero) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \nplus(\length(x),\length(\nil)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $y \in \lists{A}$ and let $a \in A$ . Now $\begin{eqnarray*} & & \length(\cat(x,\cons(a,y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \length(\cat(\snoc(a,x),y)) \\ & \hyp{\length(\cat(z,y)) = \nplus(\length(z),\length(y))} = & \nplus(\length(\snoc(a,x)),\length(y)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-snoc} = & \nplus(\next(\length(x)),\length(y)) \\ & = & \nplus(\length(x),\next(\length(y))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \nplus(\length(x),\length(\cons(a,y))) \end{eqnarray*}$ as needed.

_test_length_cat
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> t a -> Bool)
_test_length_cat _ k =
  testName "length(cat(x,y)) == plus(length(x),length(y))" $
  \x y -> eq
    ((length (cat x y)) `withTypeOf` k)
    (plus (length x) (length y))

And $\length$ detects $\nil$ .

Let $A$ be a set with $x \in \lists{A}$ . Then $x = \nil$ if and only if $\length(x) = 0$ .

We’ve already seen that $\length(\nil) = \zero$ . Suppose then that $x = \cons(a,u)$ ; then $\begin{eqnarray*} & & \length(x) \\ & \hyp{x = \cons(a,u)} = & \length(\cons(a,u)) \\ & = & \next(\length(u)); \end{eqnarray*}$ in particular, $\length(x) \neq \zero$ .

_test_length_zero
  :: (List t, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> Bool)
_test_length_zero _ k =
  testName "eq(length(x),zero) == eq(x,nil)" $
  \x -> eq
    (eq (length x) (zero `withTypeOf` k))
    (eq x nil)

Testing

Suite:

_test_length ::
  ( TypeName a, Show a, Equal a, Arbitrary a
  , TypeName n, Natural n, Equal n, Show n, Arbitrary n
  , TypeName (t a), List t, Equal (t a), Show (t a), Arbitrary (t a)
  ) => Int -> Int -> t a -> n -> IO ()
_test_length size cases t n = do
  testLabel2 "length" t n

  let args = testArgs size cases

  runTest args (_test_addlength_nil_right t n)
  runTest args (_test_addlength_cons_right t n)
  runTest args (_test_addlength_snoc_next t n)
  runTest args (_test_addlength_cons_next t n)
  runTest args (_test_addlength_rev t n)

  runTest args (_test_length_foldr t n)
  runTest args (_test_length_nil t n)
  runTest args (_test_length_cons t n)
  runTest args (_test_length_single t n)
  runTest args (_test_length_double t n)
  runTest args (_test_length_snoc t n)
  runTest args (_test_length_rev t n)
  runTest args (_test_length_cat t n)
  runTest args (_test_length_zero t n)

Main:

main_length :: IO ()
main_length = do
  _test_length 20 100 (nil :: ConsList Bool)  (zero :: Unary)
  _test_length 20 100 (nil :: ConsList Unary) (zero :: Unary)