Length

Posted on 2017-04-26 by nbloomf
Tags: arithmetic-made-difficult, literate-haskell

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:

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.\]

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

  1. \(\addlength(n,\snoc(a,x)) = \next(\addlength(n,x))\).
  2. \(\addlength(n,\cons(a,x)) = \next(\addlength(n,x))\).
  1. 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.
  2. 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.

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

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:

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.

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.\]

Special cases.

For all \(a,b \in A\), we have:

  1. \(\length(\cons(a,\nil)) = \next(\zero)\).
  2. \(\length(\cons(a,\cons(b,\nil))) = \next(\next(\zero))\).
  1. 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.
  2. 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.

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

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

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

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

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)