### CPSing anamorphisms

At the last meeting of the London Haskell User Group, my boss Peter Marks gave a talk in which he presented definitions of catamorphisms and anamorphisms such that the composition of an anamorphism followed by a catamorphism (also known as a hylomorphism) doesn’t build up an intermediate data structure.

Even though the definitions are pretty neat, the idea is not new and boils down to CPSing the definition of anamorphism. In this blog post, I’d like to illustrate on the example of lists how the CPSed definition can be derived from the standard one with the help of the Yoneda embedding (and thereby also illustrate the idea that CPS and the Yoneda embedding are the same thing).

We begin by recalling the definitions of catamorphism and anamorphism in the case of lists. We represent lists of elements of type `a`

as the fixed point of the functor `ListF a`

:

data ListF a b = Nil | Cons a b instance Functor (ListF a) where fmap _ Nil = Nil fmap f (Cons a b) = Cons a (f b) newtype Fix f = Fix { unFix :: f (Fix f) } type List a = Fix (ListF a)

Catamorphisms and anamorphisms are then defined as follows:

cata :: (ListF a b -> b) -> List a -> b cata alg = alg . fmap (cata alg) . unFix ana :: (b -> ListF a b) -> b -> List a ana coalg = Fix . fmap (ana coalg) . coalg

In his talk, Peter used a different representation of lists, which he called a *list abstraction*:

data ListAbs e v a = ListAbs (e -> v -> a) a instance Functor (ListAbs e v) where fmap f (ListAbs c n) = ListAbs (\e v -> f (c e v)) (f n) nil :: ListAbs e v a -> a nil (ListAbs _ n) = n cons :: e -> v -> ListAbs e v a -> a cons e v (ListAbs c _) = c e v

and defined catamorphisms and anamorphisms as follows:

type ListAlg e a = ListAbs e a a cataList :: ListAlg e a -> [e] -> a cataList alg = go where go (x : xs) = cons x (go xs) alg go [] = nil alg type ListCoalg v e = forall a. v -> ListAbs e v a -> a anaList :: ListCoalg v e -> v -> [e] anaList f v = f v x where x = ListAbs (\e v -> e : f v x) []

The type `ListF a b -> c`

is clearly isomorphic to the type `ListAbs a b c`

:

p :: (ListF a b -> c) -> ListAbs a b c p alg = ListAbs (\e v -> alg (Cons e v)) (alg Nil) q :: ListAbs a b c -> (ListF a b -> c) q abs (Cons e v) = cons e v abs q abs Nil = nil abs

Therefore, the type `ListF a b -> b`

is isomorphic to `ListAbs a b b`

, which by definition is equal to `ListAlg a b`

. This isomorphism allows us to translate the function `cata`

into a function

cata' :: ListAlg a b -> List a -> b cata' = cata . q

Substituting the definitions of `cata`

and `q`

and simplifying, we obtain:

cata' alg = go where go (Cons x xs) = cons x (go xs) alg go Nil = nil alg

In other words, we arrive at the definition of `cataList`

, up to the isomorphism between `List a`

and `a`

.

To relate `ana`

and `anaList`

in a similar way, we shall use the Yoneda Lemma, which claims that the type `forall b. (a -> b) -> f b`

of natural transformations from a representable functor `(->) a`

to an arbitrary functor `f`

is isomorphic to `f a`

. The isomorphism is given by a pair of mutually inverse functions:

y :: (forall b. (a -> b) -> f b) -> f a y f = f id z :: Functor f => f a -> (forall b. (a -> b) -> f b) z = flip fmap

In particular, the type `forall c. (b -> c) -> (a -> c)`

of natural transformations from a representable functor `(->) b`

to a representable functor `(->) a`

is isomorphic to the type `a -> b`

of functions from `a`

to `b`

.

By the Yoneda Lemma, the type `b -> ListF a b`

is isomorphic to the type `forall c. (ListF a b -> c) -> b -> c`

. The type `ListF a b -> c`

is isomorphic to `ListAbs a b c`

. Therefore, `b -> ListF a b`

is isomorphic to `forall c. ListAbs a b c -> b -> c`

, which up to the order of arguments is `ListCoalg a b`

. This isomorphism allows us to translate the function `ana`

into a function

ana' :: (forall c. ListAbs a b c -> b -> c) -> a -> List b ana' = ana . y . (. p)

Expanding the definitions, we obtain:

ana' f = ana ((f . p) id) = ana (f (p id)) = ana (f (ListAbs Cons Nil))

This doesn’t resemble `anaList`

yet. Here is a trick. Let us denote the function `f (ListAbs Cons Nil) :: b -> ListF a b`

by `g`

:

ana' f = ana g where g = f (ListAbs Cons Nil)

and do a bit of equational reasoning:

ana g -- definition of ana = Fix . fmap (ana g) . g -- definition of g = Fix . fmap (ana g) . f (ListAbs Cons Nil) -- definition of fmap for (->) b = fmap (Fix . fmap (ana g)) . f $ ListAbs Cons Nil -- naturality of f = f . fmap (Fix . fmap (ana g)) $ ListAbs Cons Nil -- definition of fmap for ListAbs and ListF = f $ ListAbs (\e v -> Fix (Cons e (ana g v))) (Fix Nil)

The penultimate equality is by the naturality of `f`

, which is a consequence of the free theorem associated with the polymorphic type `forall c. ListAbs a b c -> b -> c`

. We conclude that

ana' f = h where h = f $ ListAbs (\e v -> Fix (Cons e (h v))) (Fix Nil)

and you can easily convince yourself that this definition is equivalent to that of `anaList`

.