More beautiful fold zipping

My previous post, Another lovely example of type class morphisms, placed some standard structure around Max Rabkin’s Beautiful folding, using type class morphisms to confirm that the Functor and Applicative instances agreed with their inevitable meanings.

In the process of working out the Applicative case, I realized the essence of fold zipping was getting a bit obscured. This post simplifies Max’s Fold data type a bit and shows how to zip strict left folds in the simpler setting. You can get the code described here.

Edits:

  • 2008-11-15: I renamed the Pair and Pair' classes to Zip and Zip'.

A simpler fold

The strict left-folding functional is

foldl' :: (a -> b -> a) -> a -> [b] -> a

Max’s fold type packages up the first two arguments of foldl' and adds on an post-fold step, as needed for fmap:

data Fold b c = forall a. F (a -> b -> a) a (a -> c)  -- clever version

A simpler, less clever version just has the two foldl' arguments, and no forall:

data Fold b a = F (a -> b -> a) a  -- simple version

I’ll use this simpler version for zipping and later enhance it for fmap.

The strict interpretation of Fold simply unpacks and folds:

cfoldl' :: Fold b a -> [b] -> a
cfoldl' (F op e) = foldl' op e

Zipping is then just a simplification of the (<*>) definition in the previous post. As before, P is a type and constructor of strict pairs.

data P c c' = P !c !c'
 
zipF' :: Fold b a -> Fold b a' -> Fold b (P a a')
F op e `zipF'` F op' e' = F op'' (P e e')
 where
   P a a' `op''` b = P (a `op` b) (a' `op'` b)

We can also define non-strict counterparts:

cfoldl :: Fold b a -> [b] -> a
cfoldl (F op e) = foldl op e
 
zipF :: Fold b a -> Fold b a' -> Fold b (a,a')
F op e `zipF` F op' e' = F op'' (e,e')
 where
   (a,a') `op''` b = (a `op` b, a' `op'` b)

More type classes …

A previous post suggested a criterion for inevitability of interpretation functions like cfoldl and cfoldl'. Whatever class instances exists for the source type (Fold here), interpretation functions should be “type class morphisms” for those classes, which loosely means that the meaning of a method is the same method on the meaning.

Where’s the type class for our simplified Fold? It lacks the magic ingredient Max added to make it a Functor and an Applicative, namely the post-fold step.

However, there’s another class that’s just the thing:

class Zip f where zip :: f a -> f b -> f (a,b)

(I’ve used this class with type representations and user interfaces.)

The Zip class from TypeCompose is almost identical to the Zip class in category-extras. The latter class requires Functor, however, which is too restrictive for the simplified Fold type.

Our non-strict left folds have a Zip instance:

instance Zip (Fold b) where zip = zipF

For strict folds, define a strict variant on Zip:

class Zip' f where zip' :: f a -> f b -> f (P a b)

and a Zip' instance for Fold:

instance Zip' (Fold b) where zip' = zipF'

… and more morphisms

These zipping classes have associated morphism properties. A function q mapping from one Zip instance to another is a “Zip morphism” when

q (f `zip` g) == q f `zip` q g

for all folds f and g.

Similarly for Zip' morphisms:

q (f `zip'` g) == q f `zip'` q g

In other words, q distributes over zip or zip'.

As I’ll show in another post, the two interpretation functions cfoldl and cfoldl' are Zip and Zip' morphisms, respectively, i.e.,

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

which means that zip folding as defined above works correctly.

What’s next?

I like to keep blog posts fairly short, so I’ll share two more pieces of this story in upcoming blog posts:

  • Regaining the lost Functor and Applicative instances.
  • The Zip and Zip' morphism proofs for zip folding.

6 Comments

  1. Conal Elliott » Blog Archive » Enhancing a Zip:

    [...] a pattern that’s been steering me lately toward natural (inevitable) design of libraries. * Part Two simplified that representation to help get to the essence of zipping, and in doing so lost the [...]

  2. Conal Elliott » Blog Archive » Proofs for left fold zipping:

    [...] « More beautiful fold zipping Enhancing a Zip [...]

  3. Dan Piponi:

    This zip for folds is a product in the category of certain F-algebras. More generally we can write:

    import Control.Morphism.Cata
    
    prod :: Functor f => Algebra f a -> Algebra f b -> Algebra f (a,b)
    prod u v x = (u $ fmap fst x,v $ fmap snd x)
    

    which generalises this to all catamorphisms.

  4. conal:

    Thanks for the pointer, Dan. I hadn’t explored that corner of category-extras. Will look further.

    Meanwhile, here’s a tweaked definition of prod:

    prod u v = (u . fmap fst) `zip` (u . fmap snd)

    Or replace `zip` with &&&.

  5. conal:

    It recently hit me that Zip and zip aren’t such a great choice of names after all. I’d like the this notion to coincide with the Monoidal operation in section 7 of Applicative Programming with Effects, which must be consistent with Applicative instance. So the operation on lists would be cross product, not zip. On ZipList and Stream, zip is fine.

  6. Edward Kmett:

    FYI- In the newly broken out category-extras, the Apply class in semigroupoids provides the ‘Applicative-consistent’ semantics you noticed that you want for Zip here, while the Zip class in ‘keys’ provides the zip-like semantics.

Leave a comment