Conal Elliott

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)

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.

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