Conal Elliott

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.

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