## Proofs for left fold zipping

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.

1. #### Ryan Ingram:

One thing I’ve noticed about your proofs is that you play a bit fast and loose with ; the line in this proof is “We’ll want some structure on our folds as well”. Now, it’s not true that `cfoldl (undefined `zip` undefined) bs == (cfoldl undefined bs, cfoldl undefined bs)`; the former is whereas the latter is (, ). That said, I don’t really disagree with your results; I often do the same things in my informal proofs. But is there any justification for ignoring ? Can we just say “you shouldn’t use undefined folds” and leave it at that?

2. #### conal:

Ryan,

Thanks for catching and pointing out my mistake. I accidentally omitted ⊥, and I agree that my mistake is exactly where you pointed out (“We’ll want some structure ….”).

Perhaps this problem has an easy fix, using lazy pattern matching in definitions like `zipF`.

3. #### conal:

I think lazy patterns do indeed fix the ⊥ bug. For instance,

```cfoldl ~(F op e) = foldl op e

~(F op e) `zip` ~(F op' e') = F op'' (e,e')
where
~(a,a') `op''` b = (a `op` b, a' `op'` b)```

Then

`cfoldl undefined == cfoldl (F undefined undefined)`

and

```undefined `zip` f' == F undefined undefined `zip` f'

f `zip` undefined == f `zip` F undefined undefined```

So, although `undefined` does not have the form `(F op e)`, it is equivalent to such a form in the context of `cfoldl` and of `zip`, as in the morphism property:

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

I’m not sure what to make of this result. Can one always play this lazy pattern trick? I don’t think so, in the case of multiple constructors.

4. #### Conal Elliott » Blog Archive » Enhancing a Zip:

[...] Part Three proved the suitability of the zipping definitions in Part Two. [...]