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.

Advertisements