Consuming Fold
Posted on 2018-01-08 by nbloomf
\(\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.
Today we’ll implement another recursion operator on lists. This one is similar to \(\foldr(\ast)(\ast)\) but allows us to “have our cake and eat it too” in a straightforward way.
Let \(A\) and \(B\) be sets, with \(\gamma \in B\) and \(\sigma : A \times \lists{A} \times B \rightarrow B\). Then there is a unique map \(\Omega : \lists{A} \rightarrow B\) such that \[\Omega(\nil) = \gamma\] and \[\Omega(\cons(a,x)) = \sigma(a,x,\Omega(x)).\] We denote this map by \(\cfoldr(\gamma)(\sigma)\).
Define \(\varphi : A \times B^{\lists{A}} \rightarrow B^{\lists{A}}\) casewise by \[\varphi(a,g)(x) = \left\{\begin{array}{ll}
\sigma(a,\nil,g(\nil)) & \mathrm{if}\ x = \nil \\
\sigma(a,u,g(u)) & \mathrm{if}\ x = \cons(a,u),
\end{array}\right.\] and define \(\Omega(x) = \foldr(\const(\gamma))(\varphi)(x)(x)\). Note that \[\begin{eqnarray*}
& & \Omega(\nil) \\
& = & \foldr(\const(\gamma))(\varphi)(\nil)(\nil) \\
& \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil}
= & \const(\gamma)(\nil) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-const}
= & \gamma
\end{eqnarray*}\] and \[\begin{eqnarray*}
& & \Omega(\cons(a,x)) \\
& = & \foldr(\const(\gamma))(\varphi)(\cons(a,x))(\cons(a,x)) \\
& \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons}
= & \varphi(a,\foldr(\const(\gamma))(\varphi)(x))(\cons(a,x)) \\
& = & \sigma(a,x,\foldr(\const(\gamma))(\varphi)(x)(x)) \\
& = & \sigma(a,x,\Omega(x))
\end{eqnarray*}\] as needed. Suppose now that \(\Psi\) also has this property; we see that \(\Psi = \Omega\) by list induction on \(x\). For the base case \(x = \nil\) we have \[\begin{eqnarray*}
& & \Psi(\nil) \\
& = & \gamma \\
& = & \Omega(\nil),
\end{eqnarray*}\] and for the inductive step, suppose \(\Psi(x) = \Omega(x)\); then we have \[\begin{eqnarray*}
& & \Psi(\cons(a,x)) \\
& = & \sigma(a,x,\Psi(x)) \\
& = & \sigma(a,x,\Omega(a)) \\
& = & \Omega(\cons(a,x))
\end{eqnarray*}\] as needed.
Implementation
We have a few strategies for implementing \(\cfoldr(\ast)(\ast)\).
There’s the definition from the theorem:
And there’s the definition using the universal property.
We should test that the two implementations are not not equivalent.
Testing
Suite:
_test_cfoldr ::
( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
, TypeName (t a), List t, Equal (t a), Arbitrary (t a), Show (t a), CoArbitrary (t a)
) => Int -> Int -> t a -> IO ()
_test_cfoldr size cases t = do
testLabel1 "cfoldr" t
let args = testArgs size cases
runTest args (_test_cfoldr_equiv t)
Main: