# Left Fold

Posted on 2018-01-04 by nbloomf

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

{-# LANGUAGE NoImplicitPrelude #-}
module LeftFold (
foldl, _test_foldl, main_foldl
) where

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

Our goal today is to get as close as possible to a tail-recursive implementation of $$\foldr(\ast)(\ast)$$.

Let $$A$$ and $$B$$ be sets, with $$f : B \times A \rightarrow B$$. There is a unique map $$\Theta : B \times \lists{A} \rightarrow B$$ such that $\Theta(e,\nil) = e$ and $\Theta(e,\cons(a,x)) = \Theta(f(e,a),x).$ We denote this map by $$\foldl(f)$$.

First we show existence. Define $$\psi : A \times \lists{A}^B \rightarrow \lists{A}^B$$ by $\psi(a,g)(b) = g(f(b,a)),$ and define $$\Theta : B \times \lists{A} \rightarrow B$$ by $\Theta(b,x) = \foldr(\id)(\psi)(x)(b).$ Now $\begin{eqnarray*} & & \Theta(e,\nil) \\ & = & \foldr(\id)(\psi)(\nil)(e) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \id(e) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & e \end{eqnarray*}$ and $\begin{eqnarray*} & & \Theta(e,\cons(a,x)) \\ & = & \foldr(\id)(\psi)(\cons(a,x))(e) \\ & = & \psi(a,\foldr(\id)(\psi))(x)(e) \\ & = & \foldr(\id)(\psi)(x)(f(e,a)) \\ & = & \Theta(f(e,a),x) \end{eqnarray*}$ as claimed.

Now we show that $$\Theta$$ is unique with this property; to that end, suppose we have a map $$\Omega : B \times \lists{A} \rightarrow B$$ such that $$\Omega(e,\nil) = e$$ and $$\Omega(e,\cons(a,x)) = \Omega(f(e,a),x)$$ for all $$e \in B$$, $$a \in A$$, and $$x \in \lists{A}$$. We show that $$\Omega(e,x) = \Theta(e,x)$$ by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \Omega(e,\nil) \\ & = & e \\ & = & \Theta(e,\nil). \end{eqnarray*}$ For the inductive step, suppose $$\Omega(e,x) = \Theta(e,x)$$, for all $$e \in B$$ and some $$x \in \lists{A}$$, and let $$a \in A$$. Now $\begin{eqnarray*} & & \Omega(e,\cons(a,x)) \\ & = & \Omega(f(e,a),x) \\ & = & \Theta(f(e,a),x) \\ & = & \Theta(e,\cons(a,x)) \end{eqnarray*}$ as needed.

## Implementation

We have a few options for implementing $$\foldl(\ast)$$.

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

There’s the definition from the proof:

foldl' f e x = foldr id psi x e
where
psi a g b = g (f b a)

$$\psi : A \times \lists{A}^B \rightarrow \lists{A}^B$$ by $\psi(a,g)(b) = g(f(a,b)),$ and define $$\Theta : B \times \lists{A} \rightarrow B$$ by $\Theta(b,x) = \foldr(\id)(\psi)(x)(b).$

And there’s the definition from the universal property:

foldl f e z = case uncons z of
Left ()          -> e
Right (Pair a x) -> foldl f (f e a) x

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

_test_foldl_equiv :: (List t, Equal (t a), Equal a)
=> t a -> Test ((a -> a -> a) -> a -> t a -> Bool)
_test_foldl_equiv _ =
testName "foldl(f,e)(x) == foldl'(f,e)(x)" \$
\f e x -> eq (foldl f e x) (foldl' f e x)

## Testing

Suite:

_test_foldl ::
( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
, TypeName (t a), List t, Equal (t a), Arbitrary (t a), Show (t a)
) => Int -> Int -> t a -> IO ()
_test_foldl size cases t = do
testLabel1 "foldl" t

let args = testArgs size cases

runTest args (_test_foldl_equiv t)

Main:

main_foldl :: IO ()
main_foldl = do
_test_foldl 20 100 (nil :: ConsList Bool)
_test_foldl 20 100 (nil :: ConsList Unary)