# Repeat

Posted on 2017-05-22 by nbloomf

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

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

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

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.

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_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$$.

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

We proceed by induction on $$n$$. For the base case $$n = \zero$$ we have $\begin{eqnarray*} & & \length(\repeat(\zero,a)) \\ & = & \length(\nil) \\ & \href{/posts/arithmetic-made-difficult/Length.html#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{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \next(\length(\repeat(n,a))) \\ & = & \next(n) \end{eqnarray*}$ as claimed.

_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$$. 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)).$ 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{/posts/arithmetic-made-difficult/Map.html#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{/posts/arithmetic-made-difficult/Map.html#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_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$$.

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

We proceed by induction on $$m$$. For the base case $$m = \zero$$, we have $\begin{eqnarray*} & & \repeat(\nplus(\zero,n),a) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#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{/posts/arithmetic-made-difficult/Plus.html#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{/posts/arithmetic-made-difficult/Cat.html#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_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$$. 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).$ 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{/posts/arithmetic-made-difficult/Snoc.html#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{/posts/arithmetic-made-difficult/Snoc.html#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_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$$.

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

We proceed by induction on $$n$$. For the base case $$n = \zero$$, we have $\begin{eqnarray*} & & \rev(\repeat(\zero,a)) \\ & = & \rev(\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#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{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \snoc(a,\rev(\repeat(n,a))) \\ & = & \snoc(a,\repeat(n,a)) \\ & = & \repeat(\next(n),a) \end{eqnarray*}$ as needed.

_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)