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.

4 Comments

  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

    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. [...]

Leave a comment