Repeat

Posted on 2017-05-22 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 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).\]

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.

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)