## 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
`Functor`

and`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)
```

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

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

15 November 2008, 6:59 pm## David Sankel:

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

18 November 2008, 2:39 pm## 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.

18 November 2008, 8:28 pm