# Count

Posted on 2017-05-21 by nbloomf

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

{-# LANGUAGE NoImplicitPrelude #-}
module Count
) where

import Testing
import Tuples
import NaturalNumbers
import Plus
import Lists
import LeftFold
import Snoc
import Reverse
import Cat
import Length
import Filter

Today we’ll define $$\count$$, which takes an $$A$$ and a $$\lists{A}$$ and returns the number of items in the $$\lists{A}$$ that are identical to the $$A$$. As usual we’ll define this as a fold. Note that – unlike some of the other list functions we’ve seen – in principle, $$\count$$ shouldn’t care so much what order the items in its input come in. Moreover, note that $$\count$$ necessarily must examine every item in its input if it’s going to return the correct answer. When this happens – we don’t care about order but have to look at every item – the left fold operator can be used instead of the right fold, with the advantage that left fold is more space efficient.

When dealing with left folds, it is often handier to parameterize on the base case, so that’s what we’ll do.

Let $$A$$ be a set with $$a \in A$$, and define $$\varphi : \nats \times A \rightarrow \nats$$ by $\varphi(k,b) = \bif{\beq(a,b)}{\next(k)}{k}.$ Now we define $$\addcount(a) : \nats \times \lists{A} \rightarrow \nats$$ by $\addcount(a)(n,x) = \foldl(\varphi)(n)(x).$

Since $$\addcount$$ is defined as a left fold, it can be characterized as the unique solution to a system of functional equations.

Let $$A$$ be a set with $$a \in A$$. Then $$\addcount$$ is the unique map $$f : \nats \times \lists{A} \rightarrow \nats$$ satisfying the following system of equations for all $$k \in \nats$$, $$b \in A$$, and $$x \in \lists{A}$$. $\left\{\begin{array}{l} f(k,\nil) = k \\ f(k,\cons(b,x)) = f(\bif{\beq(a,b)}{\next(k)}{k},x) \end{array}\right.$

$$\addcount$$ interacts with $$\next$$.

Let $$A$$ be a set with $$a \in A$$. For all $$k \in \nats$$ and $$x \in \lists{A}$$, we have $\addcount(a)(\next(k),x) = \next(\addcount(a)(k,x)).$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \addcount(a)(\next(k),\nil) \\ & = & \next(k) \\ & = & \next(\addcount(a)(k,\nil)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$k$$ for some $$x$$ and let $$b \in A$$. Now $\begin{eqnarray*} & & \addcount(a)(\next(k),\cons(b,x)) \\ & = & \addcount(a)(\bif{\beq(a,b)}{\next(\next(k))}{\next(k)},x) \\ & = & \next(\addcount(a)(\bif{\beq(a,b)}{\next(k)}{k},x)) \\ & = & \next(\addcount(a)(k,\cons(b,x))) \end{eqnarray*}$ as needed.

Now $$\addcount$$ interacts with $$\snoc$$.

Let $$A$$ be a set with $$a \in A$$. For all $$b \in A$$ and $$x \in \lists{A}$$, we have $\addcount(a)(k,\snoc(b,x)) = \addcount(a)(\bif{\beq(a,b)}{\next(k)}{k},x).$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \addcount(a)(k,\snoc(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \addcount(a)(k,\cons(b,\nil)) \\ & = & \addcount(a)(\bif{\beq(a,b)}{\next(k)}{k},\nil) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$b$$ and $$k$$ for some $$x$$, and let $$c \in A$$. Now $\begin{eqnarray*} & & \addcount(a)(k,\snoc(b,\cons(c,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \addcount(a)(k,\cons(c,\snoc(b,x))) \\ & = & \addcount(a)(\bif{\beq(a,c)}{\next(k)}{k},\snoc(b,x)) \\ & = & \addcount(a)(\bif{\beq(a,b)}{\next(\bif{\beq(a,c)}{\next(k)}{k})}{\bif{\beq(a,c)}{\next(k)}{k}},x) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \addcount(a)(\bif{\beq(a,b)}{\bif{\beq(a,c)}{\next(\next(k))}{\next(k)}}{\bif{\beq(a,c)}{\next(k)}{k}},x) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-ifnest} = & \addcount(a)(\bif{\beq(a,c)}{\bif{\beq(a,b)}{\next(\next(k))}{\next(k)}}{\bif{\beq(a,b)}{\next(k)}{k}},x) \\ & = & \addcount(a)(\bif{\beq(a,c)}{\next(\bif{\beq(a,b)}{\next(k)}{k})}{\bif{\beq(a,b)}{\next(k)}{k}},x) \\ & = & \addcount(a)(\bif{\beq(a,b)}{\next(k)}{k},\cons(c,x)) \end{eqnarray*}$ as needed.

$$\addcount$$ interacts with $$\rev$$.

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

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

We can also characterize $$\addcount$$ as a right fold.

Let $$A$$ be a set with $$a \in A$$, and define $$\psi : A \times \nats \rightarrow \nats$$ by $\psi(b,k) = \bif{\beq(a,b)}{\next(k)}{k}.$ Then we have $\addcount(a)(k,x) = \foldr(k)(\psi)(x).$

Note that $\begin{eqnarray*} & & \addcount(a)(k,\nil) \\ & = & k \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \foldr(k)(\psi)(\nil) \end{eqnarray*}$ and $\begin{eqnarray*} & & \addcount(a)(k,\cons(b,x)) \\ & = & \addcount(a)(\bif{\beq(a,b)}{\next(k)}{k},x) \\ & = & \bif{\beq(a,b)}{\addcount(a)(\next(k),x)}{\addcount(a)(k,x)} \\ & = & \bif{\beq(a,b)}{\next(\addcount(a)(k,x))}{\addcount(a)(k,x)} \\ & = & \psi(b,\addcount(a)(k,x)). \end{eqnarray*}$ By the universal property of right fold, the equality holds for all $$x$$.

So we can evaluate $$\addcount$$ as a left fold, but reason about $$\count$$ as a right fold. Since $$\addcount(a)$$ is also a right fold, it can be characterized as the unique solution to a (different) system of functional equations.

Let $$A$$ be a set with $$a \in A$$. Now $$\addcount(a)$$ is the unique map $$f : \nats \times \lists{A} \rightarrow \nats$$ satisfying the following equations for all $$b \in A$$ and $$x \in \lists{A}$$. $\left\{\begin{array}{l} f(k,\nil) = k \\ f(k,\cons(b,x)) = \bif{\beq(a,b)}{\next(f(k,x))}{f(k,x)} \end{array}\right.$

We define $$\count$$ in terms of $$\addcount$$.

Let $$A$$ be a set with $$a \in A$$. We define $$\count : A \rightarrow \nats^{\lists{A}}$$ by $\count(a)(x) = \addcount(a)(\zero,x).$

Since $$\count$$ is defined in terms of $$\addcount$$, it is also the unique solution to a system of functional equations.

Let $$A$$ be a set with $$a \in A$$. Then $$\count(a)$$ is the unique map $$f : \lists{A} \rightarrow \nats$$ which satisfies the following system of equations for all $$b \in A$$ and $$x \in \lists{A}$$. $\left\{\begin{array}{l} f(\nil) = \zero \\ f(\cons(b,x)) = \bif{\beq(a,b)}{\next(f(x))}{f(x)} \end{array}\right.$

A special case.

Let $$A$$ be a set, with $$a,b \in A$$. Then $\count(a,\cons(b,\nil)) = \bif{\beq(a,b)}{\next(\zero)}{\zero}.$

Note that $\begin{eqnarray*} & & \count(a,\cons(b,\nil)) \\ & = & \foldl(\zero){\varphi(a)}(\cons(b,\nil)) \\ & = & \foldl(\varphi(a)(b,\zero)){\varphi(a)}(\nil) \\ & = & \varphi(a)(b,\zero) \\ & = & \bif{\beq(a,b)}{\next(\zero)}{\zero} \end{eqnarray*}$ as claimed.

$$\count$$ interacts with $$\snoc$$.

Let $$A$$ be a set with $$a \in A$$. For all $$b \in A$$ and $$x \in \lists{A}$$, we have $\count(a)(\snoc(b,x)) = \bif{\beq(a,b)}{\next(\count(a)(x))}{\count(a)(x)}.$

Note that $\begin{eqnarray*} & & \count(a)(\snoc(b,x)) \\ & = & \addcount(a)(\zero,\snoc(b,x)) \\ & = & \bif{\beq(a,b)}{\next(\addcount(a)(\zero,x))}{\addcount(a)(\zero,x)} \\ & = & \bif{\beq(a,b)}{\next(\count(a)(x))}{\count(a)(x)} \end{eqnarray*}$ as claimed.

$$\count$$ interacts with $$\rev$$.

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

Note that $\begin{eqnarray*} & & \count(a)(\rev(x)) \\ & = & \addcount(a)(\zero,\rev(x)) \\ & = & \addcount(a)(\zero,x) \\ & = & \count(a)(x) \end{eqnarray*}$ as claimed.

$$\count$$ interacts with $$\cat$$.

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

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \count(a,\cat(x,y)) \\ & = & \count(a,\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \count(a,y) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-zero} = & \nplus(\zero,\count(a,y)) \\ & = & \nplus(\count(a,\nil),\count(a,y)) \\ & = & \nplus(\count(a,x),\count(a,y)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$y$$ and $$a$$ for some $$x$$, and let $$b \in A$$. We consider two possibilities. If $$a = b$$, we have $\begin{eqnarray*} & & \count(a,\cat(\cons(b,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \count(a,\cons(b,\cat(x,y))) \\ & = & \bif{\beq(a,b)}{\next(\count(a,\cat(x,y)))}{\count(a,\cat(x,y))} \\ & = & \next(\count(a,\cat(x,y))) \\ & = & \next(\nplus(\count(a,x),\count(a,y))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \nplus(\next(\count(a,x)),\count(a,y)) \\ & = & \nplus(\bif{\beq(a,b)}{\next(\count(a,x))}{\count(a,x)},\count(a,y)) \\ & = & \nplus(\count(a,\cons(b,x)),\count(a,y)) \end{eqnarray*}$ as needed. If $$a \neq b$$, we have $\begin{eqnarray*} & & \count(a,\cat(\cons(b,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \count(a,\cons(b,\cat(x,y))) \\ & = & \bif{\beq(a,b)}{\next(\count(a,\cat(x,y)))}{\count(a,\cat(x,y))} \\ & = & \count(a,\cat(x,y)) \\ & = & \nplus(\count(a,x),\count(a,y)) \\ & = & \nplus(\bif{\beq(a,b)}{\next(\count(a,x))}{\count(a,x)},\count(a,y)) \\ & = & \nplus(\count(a,\cons(b,x)),\count(a,y)) \end{eqnarray*}$ as needed.

$$\count$$ is a $$\length$$.

Let $$A$$ be a set. We have $\count(a,x) = \length(\filter(\beq(a,-),x)).$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \count(a,x) \\ & = & \count(a,\nil) \\ & = & \foldr(\zero)(\varphi(a))(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \zero \\ & = & \length(\nil) \\ & = & \length(\filter(\beq(a,-),\nil)) \\ & = & \length(\filter(\beq(a,-),x)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x$$ and let $$b \in A$$. We consider two possibilities. If $$a = b$$, we have $\begin{eqnarray*} & & \count(a,\cons(b,x)) \\ & = & \count(a,\cons(a,x)) \\ & = & \bif{\beq(a,a)}{\next(\count(a,x))}{\count(a,x)} \\ & = & \next(\count(a,x)) \\ & = & \next(\length(\filter(\beq(a,-),x))) \\ & = & \length(\cons(a,\filter(\beq(a,-),x))) \\ & = & \length(\filter(\beq(a,-),\cons(a,x))) \end{eqnarray*}$ as needed. If $$a \neq b$$, we have $\begin{eqnarray*} & & \count(a,\cons(b,x)) \\ & = & \bif{\beq(a,b)}{\next(\count(a,x))}{\count(a,x)} \\ & = & \count(a,x) \\ & = & \length(\filter(\beq(a,-),x)) \\ & = & \length(\filter(\beq(a,-),\cons(b,x))) \end{eqnarray*}$ as needed.

$$\count$$ interacts with $$\map(f)$$ when $$f$$ is injective.

Let $$A$$ and $$B$$ be sets and $$f : A \rightarrow B$$ an injective map. Then $\count(a,x) = \count(f(a),\map(f)(x)).$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \count(a,x) \\ & = & \count(a,\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \count(a,\map(f)(\nil)) \\ & = & \count(a,\map(f)(x)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x$$, and let $$b \in A$$. We consider two possibilities. If $$a = b$$, then $$f(a) = f(b)$$, and we have $\begin{eqnarray*} & & \count(a,\cons(b,x)) \\ & = & \count(a,\cons(a,x)) \\ & = & \next(\count(a,x)) \\ & = & \next(\count(f(a),\map(f)(x))) \\ & = & \count(f(a),\cons(f(a),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \count(f(a),\map(f)(\cons(a,x))) \\ & = & \count(f(a),\map(f)(\cons(b,x))) \end{eqnarray*}$ as needed. If $$a \neq b$$, then we have $$f(a) \neq f(b)$$ (since $$f$$ is injective), so that $\begin{eqnarray*} & & \count(a,\cons(b,x)) \\ & = & \count(a,x) \\ & = & \count(f(a),\map(f)(x)) \\ & = & \count(f(a),\cons(f(b),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \count(f(a),\map(f)(\cons(b,x))) \end{eqnarray*}$ as needed.

## Testing

Suite:

_test_count ::
( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
, TypeName (t a), List t
, TypeName n, Natural n, Equal n, Show n, Arbitrary n
, Show (t a), Equal (t a), Arbitrary (t a), Equal (t (Pair a a))
) => Int -> Int -> t a -> n -> IO ()
_test_count size cases t n = do
testLabel2 "count" t n

let args = testArgs size cases

runTest args (_test_count_nil t n)
runTest args (_test_count_cons t n)
runTest args (_test_count_one t n)
runTest args (_test_count_snoc t n)
runTest args (_test_count_rev t n)
runTest args (_test_count_cat t n)
runTest args (_test_count_length t n)

Main:

main_count :: IO ()
main_count = do
_test_count 20 100 (nil :: ConsList Bool)  (zero :: Unary)
_test_count 20 100 (nil :: ConsList Unary) (zero :: Unary)