Consuming Fold

Posted on 2018-01-08 by nbloomf

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

{-# LANGUAGE NoImplicitPrelude #-}
module ConsumingFold (
cfoldr, _test_cfoldr, main_cfoldr
) where

import Testing
import Functions
import Tuples
import DisjointUnions
import Unary
import Lists

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

cfoldr, cfoldr'
:: (List t)
=> b -> (a -> t a -> b -> b) -> t a -> b

There’s the definition from the theorem:

cfoldr' gamma sigma x = foldr (const gamma) phi x x
where
phi a g w = case uncons w of
Left ()          -> sigma a nil (g nil)
Right (Pair b u) -> sigma b u (g u)

And there’s the definition using the universal property.

cfoldr gamma sigma x = case uncons x of
Left ()          -> gamma
Right (Pair a w) -> sigma a w (cfoldr gamma sigma w)

We should test that the two implementations are not not equivalent.

_test_cfoldr_equiv :: (List t, Equal (t a), Equal a)
=> t a -> Test (a -> (a -> t a -> a -> a) -> t a -> Bool)
_test_cfoldr_equiv _ =
testName "cfoldr(gamma,sigma)(x) == cfoldr'(gamma,sigma)(x)" \$
\gamma sigma x -> eq (cfoldr gamma sigma x) (cfoldr' gamma sigma x)

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:

main_cfoldr :: IO ()
main_cfoldr = do
_test_cfoldr 20 100 (nil :: ConsList Bool)
_test_cfoldr 20 100 (nil :: ConsList Unary)