Enhancing a Zip

This post is part four of the zip folding series inspired by Max Rabkin’s Beautiful folding post. I meant to write one little post, but one post turned into four. When I sense that something can be made simpler/clearer, I can’t leave it be.

To review:

  • Part One related Max’s data representation of left folds to type class morphisms, 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 expressiveness necessary to define Functorand Applicative instaces.
  • Part Three proved the suitability of the zipping definitions in Part Two.

This post shows how to restore the Functor and Applicative (very useful composition tools) to folds but does so in a way that leaves the zipping functionality untouched. This new layer is independent of folding and can be layered onto any zippable type.

You can get the code described below.

Edits:

  • 2009-02-15: Simplified WithCont, collapsing two type parameters into one. Added functor comment about cfoldlc'.

What’s missing?

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

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

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

Removing Max’s post-fold step gets to the essence of fold zipping but loses some useful composability. In particular, we can no longer define Functor and Applicative instances.

The difference between the clever version and the simple one is a continuation and a forall, which we can write down as follows:

data WithCont z c = forall a. WC (z a) (a -> c)

The clever version is equivalent to the following:

type FoldC b = WithCont (Fold b)

Interpretating a FoldC just interprets the Fold and then applies the continuation:

cfoldlc :: FoldC b a -> [b] -> a
cfoldlc (WC f k) = k . cfoldl f

(In a more general setting, use fmap in place of (.) to give meaning to WithCont.)

Add a copy of WithCont, for reasons explained later, and use it for strict folds.

data WithCont' z c = forall a. WC' (z a) (a -> c)
 
type FoldC' b = WithCont' (Fold b)
 
cfoldlc' :: FoldC' b a -> [b] -> a
cfoldlc' (WC' f k) = k . cfoldl' f

From Zip to Functor and Applicative

It’s now a simple matter to recover the lost Functor and Applicative instances, for both non-strict and strict zipping. The Applicative instances rely on zippability:

instance Functor (WithCont z) where
  fmap g (WC f k) = WC f (g . k)
 
instance Zip z => Applicative (WithCont z) where
  pure a = WC undefined (const a)
  WC hf hk <*> WC xf xk =
    WC (hf `zip` xf) (\ (a,a') -> (hk a) (xk a'))
 
 
instance Functor (WithCont' z) where
  fmap g (WC' f k) = WC' f (g . k)
 
instance Zip' z => Applicative (WithCont' z) where
  pure a = WC' undefined (const a)
  WC' hf hk <*> WC' xf xk =
    WC' (hf `zip'` xf) (\ (P a a') -> (hk a) (xk a'))

Now the reason for the duplicate WithCont definition becomes apparent. Instance selection in Haskell is based entirely on the “head” of an instance. If both Applicative instances used WithCont, the compiler would consider them to overlap.

Morphism proofs

It remains to prove that our interpretation functions are Functor and Applicative morphisms. I’ll show the non-strict proofs. The strict morphism proofs go through similarly.

Functor

The Functor morphism property for non-strict folding:

cfoldlc (fmap g wc) == fmap g (cfoldlc wc)

Adding some structure:

cfoldlc (fmap g (WC f k)) == fmap g (cfoldlc (WC f k))

Proof:

cfoldlc (fmap g (WC f k))
 
  == {- fmap on WithCont -}
 
cfoldlc (WC f (g . k))
 
  == {- cfoldlc def -}
 
(g . k) . cfoldl f
 
  == {- associativity of (.)  -}
 
g . (k . cfoldl f)
 
  == {- cfoldl def -}
 
g . cfoldlc (WC f k)
 
  == {- fmap on functions -}
 
fmap g (cfoldlc (WC f k))

Applicative

Applicative has two methods, so cfoldlc must satisfy two morphism properties. One for pure:

cfoldlc (pure a) == pure a

Proof:

cfoldlc (pure a)
 
  == {- pure on WithCont -}
 
cfoldlc (WC undefined (const a))
 
  == {- cfoldlc def -}
 
const a . cfoldl undefined
 
  == {- property of const -}
 
const a
 
  == {- pure on functions -}
 
pure a

And one for (<*>):

cfoldlc (wch <*> wcx) == cfoldlc wch <*> cfoldlc wcx

Adding structure:

cfoldlc ((WC hf hk) <*> (WC xf xk)) == cfoldlc (WC hf hk) <*> cfoldlc (WC xf xk)

Proof:

cfoldlc ((WC hf hk) <*> (WC xf xk))
 
  == {- (<*>) on WithCont -}
 
cfoldlc (WC (hf `zip` xf) (\ (a,a') -> (hk a) (xk a')))
 
  == {- cfoldlc def -}
 
(\ (a,a') -> (hk a) (xk a')) . cfoldl (hf `zip` xf)
 
  == {- Zip morphism law for Fold -}
 
(\ (a,a') -> (hk a) (xk a')) . (cfoldl hf `zip` cfoldl xf)
 
  == {- zip def on functions -}
 
(\ (a,a') -> (hk a) (xk a')) . \ bs -> (cfoldl hf bs, cfoldl xf bs)
 
  == {- (.) def -}
 
\ bs -> (hk (cfoldl hf bs)) (xk (cfoldl xf bs))
 
  == {- (<*>) on functions -}
 
(hk . cfoldl hf bs) <*> (xk . cfoldl xf)
 
  == {- cfoldlc def, twice -}
 
cfoldlc (WC hf hk) <*> cfoldlc (WC xf xk)

That’s it.

I like that WithCont allows composing the morphism proofs, in addition to the implementations.

3 Comments

  1. Creighton:

    Hey Conal, I’ve liked this series of posts as well as the original article that inspired them. I’ve started getting back into category theory, re-reading my MacLane & all that, and I’m wondering if the lesson that should be taken from your thoughts on this combined with this old post post is that we need to go beyond just being “functional” programmers & be “algebraic” programmers concerned with notions of naturalness. I know there were a lot of papers by Meijer et. al. back in the day about the algebraic connections to programming, but maybe it should be a practical part of any library design.

    I have a feeling you’re going to say “well, yes, duh” but it’s just striking to me how we might be able to gain a lot of modularity by clearly elucidating the categoric properties of an interface.

  2. David Sankel:

    Conal, thanks for the series of posts. It is a good exposition of your methods of reducing redundancy to the bare minimum.

  3. Michael:

    RE: Creighton

    Worth noting that it’s not just us functional folks who are interested in algebraic structure. Stepanov, the man behind the C++ STL, has made a career out of it, and has a book in the works from the imperative side of the fence that presents programming as mathematical abstraction. See the following for the current draft:

    http://www.stepanovpapers.com/eop/eop.pdf

    Seems all the smart guys are into it these days ;) Neat stuff.

Leave a comment