Conal Elliott

The post More beautiful fold zipping showed a formulation of left-fold zipping, simplified from the ideas in Max Rabkin’s Beautiful folding. I claimed that the semantic functions are the inevitable (natural) ones in that they preserve zipping stucture. This post gives the promised proofs.

The correctness of fold zipping can be expressed as follows. Is cfoldl a Zip morphism, and is cfoldl' a Zip' morphism? (See More beautiful fold zipping for definitions of these functions and classes, and see Simplifying semantics with type class morphisms for the notion of type class morphisms.)

Non-strict

The non-strict version is simpler, though less useful. We want to prove

cfoldl (f `zip` f') == cfoldl f `zip` cfoldl f'

First, substitute the definition of zip for functions.

instance Zip ((->) u) where zip = liftA2 (,)

This definition is a standard one for zipping applicative functors. Given the Applicative instance for functions, this Zip instance is equivalent to

instance Zip ((->) u) where r `zip` s =  u -> (r u, s u)

So the Zip morphism property becomes

cfoldl (f `zip` f') bs == (cfoldl f bs, cfoldl f' bs)

We’ll want some structure to our folds as well:

cfoldl (F op e `zip` F op' e') bs
  == (cfoldl (F op e) bs, cfoldl (F op' e') bs)

Simplify the LHS:

cfoldl (F op e `zip` F op' e') bs

  == {- Fold zip def -}

cfoldl (F op'' (e,e')) bs
  where (a,a') `op''` b = (a `op` b, a' `op'` b)

  == {- cfoldl def -}

foldl op'' (e,e') bs
  where (a,a') `op''` b = (a `op` b, a' `op'` b)

Then simplify the RHS:

(cfoldl (F op e) bs, cfoldl (F op' e') bs)

  == {- cfoldl def -}

(foldl op e bs, foldl op' e' bs)

So the morphism law becomes

foldl op'' (e,e') bs == (foldl op e bs, foldl op' e' bs)
  where
    (a,a') `op''` b = (a `op` b, a' `op'` b)

We’ll prove this form inductively in the list bs, using the definition of foldl:

foldl :: (a -> b -> a) -> a -> [b] -> a
foldl op a []     = a
foldl op a (b:bs) = foldl op (a `op` b) bs

First, empty lists.

foldl op'' (e,e') [] where op'' = ...

  == {- foldl def  -}

(e,e')

  == {- foldl def, twice -}

(foldl op e [], foldl op' e' [])

Next, non-empty lists.

foldl op'' (e,e') (b:bs) where op'' = ...

  == {- foldl def -}

foldl op'' ((e,e') `op''` b) bs where op'' = ...

  == {- op'' definition -}

foldl op'' (e `op` b, e' `op'` b) bs where op'' = ...

  == {- induction hypothesis -}

(foldl op (e `op` b) bs, foldl op' (e' `op'` b) bs)

  == {- foldl def, twice -}

(foldl op e (b:bs), foldl op' e' (b:bs))

Strict

The morphism law:

cfoldl' (f `zip'` f') == cfoldl' f `zip'` cfoldl' f'

which simplifies to

foldl' op'' (P e e') bs == P (foldl' op e bs) (foldl' op' e' bs)
  where
    P a a' `op''` b = P (a `op` b) (a' `op'` b)

This property can be proved similarly to the non-strict version. The new aspect is manipulating the use of seq.

Again, use induction on lists, guided by the fold definition:

foldl' :: (a -> b -> a) -> a -> [b] -> a
foldl' op a []     = a
foldl' op a (b:bs) =
  let a' = a `op` b in a' `seq` foldl' f a' bs

First, empty lists.

foldl op'' (P e e') [] where op'' = ...

  == {- foldl def  -}

P e e'

  == {- foldl def, twice -}

P (foldl op e []) (foldl op' e' [])

Next, non-empty lists. For simplicity, I’ll inline the let in the definition of foldl' (which affects performance but not meaning):

foldl' op'' (P e e') (b:bs) where op'' = ...

  == {- foldl' def -}

((P e e') `op''` b) `seq`
foldl' op'' ((P e e') `op''` b) bs where op'' = ...

  == {- op'' definition -}

P (e `op` b) (e' `op'` b) `seq`
foldl' op'' (P (e `op` b) (e' `op'` b)) bs

  == {- induction hypothesis -}

P (e `op` b) (e' `op'` b) `seq`
P (foldl' op (e `op` b) bs) (foldl' op' (e' `op` b) bs)

  == {- P strictness -}

P (e `op` b) (e' `op'` b) `seq`
P ((e  `op` b) `seq` foldl' op  (e  `op` b) bs)
  ((e' `op` b) `seq` foldl' op' (e' `op` b) bs)

  == {- foldl' def, twice -}

P (foldl' op e (b:bs)) (foldl' op' e' (b:bs))

That’s it.

The post More beautiful fold zipping showed a formulation of left-fold zipping, simplified from the ideas in Max Rabkin’s Beautiful folding. I claimed that the semantic functions are the inevitable...