---
title: Repeat
author: nbloomf
date: 2017-05-22
tags: arithmetic-made-difficult, literate-haskell
slug: repeat
---

> {-# LANGUAGE NoImplicitPrelude #-}
> module Repeat
>   ( repeat, _test_repeat, main_repeat
>   ) where
> 
> import Testing
> import Tuples
> import DisjointUnions
> import NaturalNumbers
> import Plus
> import Lists
> import Snoc
> import Reverse
> import Cat
> import Length
> import Map
> import UnfoldN

So far we've defined a bunch of functions that operate on lists, but still only one that can create one out of nothing, namely $\range$. ($\tails$ and $\inits$ create lists, but only if we have one to start with.) Today we'll nail down another list-creating utility, $\repeat$.

:::::: definition ::
Let $A$ be a set, and define $f : A \rightarrow 1 + A \times A$ by $f(x) = \rgt((x,x))$. Now define $\repeat : \nats \rightarrow {\lists{A}}^A$ by $$\repeat(n)(a) = \unfoldN(f)(n,a).$$

In Haskell:

> repeat :: (List t, Natural n) => n -> a -> t a
> repeat n a = unfoldN f n a
>   where
>     f x = rgt (tup x x)

::::::::::::::::::::

Since $\repeat$ is defined as an unfoldN, it is the unique solution to a system of functional equations.

:::::: corollary :::
Let $A$ be a set. Then $\repeat$ is the unique map $f : \nats \rightarrow {\lists{A}}^A$ satisfying the following equations for all $n \in \nats$ and $a \in A$.
$$\left\{\begin{array}{l}
 f(\zero)(a) = \nil \\
 f(\next(n))(a) = \cons(a,f(n)(a))
\end{array}\right.$$

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\repeat$ is kind of boring. I'm not sure if we'll actually need these, but here are some interactions using $\repeat$.

$\repeat$ and $\length$.

:::::: theorem :::::
Let $A$ be a set. For all $n \in \nats$ and $a \in A$ we have $$\length(\repeat(n,a)) = n.$$

::: proof ::::::::::
We proceed by induction on $n$. For the base case $n = \zero$ we have
$$\begin{eqnarray*}
 &   & \length(\repeat(\zero,a)) \\
 & = & \length(\nil) \\
 &     \href{@length@#cor-length-nil}
   = & \zero
\end{eqnarray*}$$
as claimed. For the inductive step, suppose the equality holds for some $n$. Then we have
$$\begin{eqnarray*}
 &   & \length(\repeat(\next(n),a)) \\
 & = & \length(\cons(a,\repeat(n,a))) \\
 &     \href{@length@#cor-length-cons}
   = & \next(\length(\repeat(n,a))) \\
 & = & \next(n)
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\repeat$ and $\map$.

:::::: theorem :::::
Let $A$ and $B$ be sets with $f : A \rightarrow B$ a map. For all $n \in \nats$ and $a \in A$, we have $$\map(f)(\repeat(n,a)) = \repeat(n,f(a)).$$

::: proof ::::::::::
We proceed by induction on $n$. For the base case $n = \zero$ we have
$$\begin{eqnarray*}
 &   & \map(f)(\repeat(\zero,a)) \\
 & = & \map(f)(\nil) \\
 &     \href{@map@#cor-map-nil}
   = & \nil \\
 & = & \repeat(\zero,f(a))
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for some $n$. Now we have
$$\begin{eqnarray*}
 &   & \map(f)(\repeat(\next(n),a)) \\
 & = & \map(f)(\cons(a,\repeat(n,a))) \\
 &     \href{@map@#cor-map-cons}
   = & \cons(f(a),\map(f)(\repeat(n,a))) \\
 & = & \cons(f(a),\repeat(n,f(a))) \\
 & = & \repeat(\next(n),f(a))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_repeat_map :: (List t, Equal a, Equal b, Natural n, Equal n, Equal (t b))
>   => t a -> t b -> n -> Test ((a -> b) -> n -> a -> Bool)
> _test_repeat_map t _ _ =
>   testName "map(f)(repeat(n,a)) == repeat(n,f(a))" $
>   \f k a -> eq
>     (repeat k (f a))
>     (map f (repeat k a `withTypeOf` t))

::::::::::::::::::::
::::::::::::::::::::

$\repeat$ and $\nplus$.

:::::: theorem :::::
Let $A$ be a set. For all $m,n \in \nats$ and $a \in A$, we have $$\repeat(\nplus(m,n),a) = \cat(\repeat(m,a),\repeat(n,a)).$$

::: proof ::::::::::
We proceed by induction on $m$. For the base case $m = \zero$, we have
$$\begin{eqnarray*}
 &   & \repeat(\nplus(\zero,n),a) \\
 &     \href{@plus@#cor-plus-up-zero}
   = & \repeat(n,a) \\
 & = & \cat(\nil,\repeat(n,a)) \\
 & = & \cat(\repeat(\zero,a),\repeat(n,a))
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for some $m$. Now we have
$$\begin{eqnarray*}
 &   & \repeat(\nplus(\next(m),n),a) \\
 &     \href{@plus@#cor-plus-up-next}
   = & \repeat(\next(\nplus(m,n)),a) \\
 & = & \cons(a,\repeat(\nplus(m,n),a)) \\
 & = & \cons(a,\cat(\repeat(m,a),\repeat(n,a))) \\
 &     \href{@cat@#cor-cat-cons}
   = & \cat(\cons(a,\repeat(m,a)),\repeat(n,a)) \\
 & = & \cat(\repeat(\next(m),a),\repeat(n,a))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_repeat_plus :: (List t, Equal a, Natural n, Equal n, Equal (t a))
>   => t a -> n -> Test (n -> n -> a -> Bool)
> _test_repeat_plus t _ =
>   testName "repeat(plus(m,n),a) == cat(repeat(m,a),repeat(n,a))" $
>   \m n a -> eq
>     ((repeat (plus m n) a) `withTypeOf` t)
>     (cat (repeat m a) (repeat n a))

::::::::::::::::::::
::::::::::::::::::::

$\repeat$ and $\snoc$.

:::::: theorem :::::
Let $A$ be a set. For all $n \in \nats$ and $a \in A$, we have $$\snoc(a,\repeat(n,a)) = \repeat(\next(n),a).$$

::: proof ::::::::::
We proceed by induction on $n$. For the base case $n = \zero$, we have
$$\begin{eqnarray*}
 &   & \snoc(a,\repeat(\zero)(a)) \\
 & = & \snoc(a,\nil) \\
 &     \href{@snoc@#cor-snoc-nil}
   = & \cons(a,\nil) \\
 & = & \cons(a,\repeat(\zero)(a)) \\
 & = & \repeat(\next(n))(a)
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for some $n$. Now we have
$$\begin{eqnarray*}
 &   & \snoc(a,\repeat(\next(n))(a)) \\
 & = & \snoc(a,\cons(a,\repeat(n)(a))) \\
 &     \href{@snoc@#cor-snoc-cons}
   = & \cons(a,\snoc(a,\repeat(n)(a))) \\
 & = & \cons(a,\repeat(\next(n))(a)) \\
 & = & \repeat(\next(\next(n)))(a)
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\repeat$ and $\rev$.

:::::: theorem :::::
Let $A$ be a set. For all $n \in \nats$ and $a \in A$, we have $$\rev(\repeat(n,a)) = \repeat(n,a).$$

::: proof ::::::::::
We proceed by induction on $n$. For the base case $n = \zero$, we have
$$\begin{eqnarray*}
 &   & \rev(\repeat(\zero,a)) \\
 & = & \rev(\nil) \\
 &     \href{@rev@#cor-rev-nil}
   = & \nil \\
 & = & \repeat(\zero,a)
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for some $n$. Then we have
$$\begin{eqnarray*}
 &   & \rev(\repeat(\next(n),a)) \\
 & = & \rev(\cons(a,\repeat(n,a))) \\
 &     \href{@rev@#cor-rev-cons}
   = & \snoc(a,\rev(\repeat(n,a))) \\
 & = & \snoc(a,\repeat(n,a)) \\
 & = & \repeat(\next(n),a)
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::


Testing
-------

Suite:

> _test_repeat ::
>   ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
>   , TypeName b, Equal b, Show b, Arbitrary b, CoArbitrary b
>   , TypeName (t a), List t
>   , TypeName n, Natural n, Arbitrary n, Show n, Equal n
>   , Show (t a), Equal (t a), Arbitrary (t a), Equal (t (Pair a a)), Equal (t b)
>   ) => Int -> Int -> t a -> t b -> n -> IO ()
> _test_repeat size cases t u n = do
>   testLabel2 "repeat" t n
> 
>   let args = testArgs size cases
> 
>   runTest args (_test_repeat_zero t n)
>   runTest args (_test_repeat_next t n)
>   runTest args (_test_repeat_length t n)
>   runTest args (_test_repeat_map t u n)
>   runTest args (_test_repeat_plus t n)
>   runTest args (_test_repeat_snoc t n)
>   runTest args (_test_repeat_rev t n)

Main:

> main_repeat :: IO ()
> main_repeat = do
>   _test_repeat 20 100 (nil :: ConsList Bool)  (nil :: ConsList Bool)  (zero :: Unary)
>   _test_repeat 20 100 (nil :: ConsList Unary) (nil :: ConsList Unary) (zero :: Unary)