Category Theory Helpline

by oleksandrmanzyuk

One of my colleagues, Ben Moseley, has recently asked an interesting category theoretic question. I’ve decided to write up my answer in a blog post.

Preliminaries

This blog post is a literate Haskell program. First, we are going to enable a few language extensions and import a few modules:

> {-# LANGUAGE FlexibleInstances     #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE TupleSections         #-}
> {-# LANGUAGE TypeOperators         #-}
> import Control.Arrow
> import Data.Traversable
> import Prelude hiding (sequence)

Next, we are going to recall the definitions of the fixed point of a functor f, the free monad generated by f, and the cofree comonad generated by f:

> newtype Fix f = Fix { unFix :: f (Fix f) }
> data Free f a = Pure a | Free (f (Free f a))
> data Cofree f a = a :< f (Cofree f a)

All three definitions are fairly standard. The last two can be found, for example, in Edward Kmett’s package free.

Fix f is both an initial algebra and final coalgebra for f: the f-algebra structure is given by Fix :: f (Fix f) -> Fix f, and the f-coalgebra structure is given by unFix :: Fix f -> f (Fix f).

The initiality means that for each f-algebra alg :: f a -> a there exists a unique f-algebra morphism cata alg :: Fix f -> a, called catamorphism. cata alg being an f-algebra morphism means that the following equation holds:

cata alg . Fix == alg . fmap (cata alg)

from which we can read off the definition of cata alg:

> cata :: Functor f => (f a -> a) -> Fix f -> a
> cata alg = alg . fmap (cata alg) . unFix

Similarly, the finality means that for each f-coalgebra coalg :: a -> f a there exists a unique f-coalgebra morphism ana coalg :: a -> Fix f, called anamorphism. ana coalg being an f-coalgebra morphism means that the following equation holds:

unFix . ana coalg == fmap (ana coalg) . coalg

from which we can read off the definition of ana coalg:

> ana :: Functor f => (a -> f a) -> a -> Fix f
> ana coalg = Fix . fmap (ana coalg) . coalg

The original version of this blog post fell into the fallacy of claiming that every function from resp. to Fix f could be expressed a catamorphism resp. an anamorphism. This is obviously not the case. “When is a function a fold or an unfold?” by Jeremy Gibbons, Graham Hutton, and Thorsten Altenkirch gives necessary and sufficient conditions for when a set-theoretic function can be written as a catamorphism resp. an anamorphism (thanks to Ben for pointing this out). The fallacy doesn’t affect the calculations below. However, they become somewhat less natural than I originally thought.

The functions cata and ana are only two examples of the plethora of recursion schemes associated with the type Fix f. The types Free f a and Cofree f a also have associated recursion schemes:

> fold :: Functor f => (Either a (f b) -> b) -> Free f a -> b
> fold f m = f $ case m of
>   Pure x -> Left x
>   Free n -> Right $ fmap (fold f) n

> unfold :: Functor f => (b -> (a, f b)) -> b -> Cofree f a
> unfold f c = case f c of
>   (x, d) -> x :< fmap (unfold f) d

The question

Ben wrote the following functions:

> cofree2fix :: Functor f => Cofree f a -> Fix f
> cofree2fix = ana (\(_ :< fx) -> fx)

> fix2free :: Functor f => Fix f -> Free a
> fix2free = cata Free

> fix2cofree :: Functor f => (a, Fix f) -> Cofree f a
> fix2cofree (a, fx) = unfold (const a &&& unFix) fx

> free2fix :: Traversable f => Free f a -> Either a (Fix f)
> free2fix = fold (Left ||| (right Fix . sequence))

Here

(&&&) :: (a -> b) -> (a -> c) -> a -> (b, c)

and

(|||) :: (b -> d) -> (c -> d) -> Either b c -> d

are the standard mediating morphisms for products and sums. They are imported from Control.Arrow. The function sequence is the generalized version from Data.Traversable.

Ben then wrote:

I’m puzzled by the last one… It all typechecks, but there’s a clear asymmetry between fix2cofree and free2fix which worries me…

The rest of this blog post is an attempt to explain what is going on here.

It’s fixed points all the way down

We first observe that Free f a is isomorphic to the fixed point of the functor Either a :. f, and Cofree f a is isomorphic to the fixed point of the functor (,) a :. f, where :. denotes functor composition (thanks to Roman Cheplyaka for suggesting this notation):

> newtype (f :. g) a = C { unC :: f (g a) }

> instance (Functor f, Functor g) => Functor (f :. g) where
>   fmap t (C x) = C $ fmap (fmap t) x

We can encode isomorphisms between types by means of a typeclass, Iso:

> class Iso a b where
>   iso :: a -> b
>   inv :: b -> a

The isomorphisms between Free f a and Fix (Either a :. f), and between Cofree f a and Fix ((,) a :. f) are then defined as follows:

> instance Functor f => Iso (Free f a) (Fix (Either a :. f)) where
>   iso = fold (Fix . C)
>   inv = cata (either Pure Free . unC)

> instance Functor f => Iso (Cofree f a) (Fix ((,) a :. f)) where
>   iso = ana (\(x :< fx) -> C (x, fx))
>   inv = unfold (unC . unFix)

Under this identification, the recursion schemes fold and unfold identify with cata and ana respectively.

We shall show now that the functions cofree2fix, fix2free, fix2cofree, and free2fix can naturally be expressed as cata- resp. anamorphisms of some naturally arising algebras resp. coalgebras over the functor f.

cofree2fix

The finality of Fix f allows us to manufacture a function

Fix ((,) a :. f) -> Fix f

out of a function

Fix ((,) a :. f) -> f (Fix ((,) a :. f))

There is an obvious natural representative of the latter type, namely the composite snd . unC . unFix, leading to the following definition:

> cofree2fix' :: Functor f => Fix ((,) a :. f) -> Fix f
> cofree2fix' = ana (snd . unC . unFix)

fix2free

The initiality of Fix f implies that each function

f (Fix (Either a :. f)) -> Fix (Either a :. f)

gives rise to a function

Fix f -> Fix (Either a :. f)

There is an obvious natural representative of the former type, namely the composite Fix . C . Right, which corresponds to the constructor Free under the isomorphism between Free f a and Fix (Either a :. f). Therefore, we can define

> fix2free' :: Functor f => Fix f -> Fix (Either a :. f)
> fix2free' = cata (Fix . C . Right)

fix2cofree

By the finality of Fix ((,) a :. f), we obtain a function

(a, Fix f) -> Fix ((,) a :. f)

from each function

(a, Fix f) -> ((,) a :. f) (a, Fix f)

The type ((,) a :. f) (a, Fix f) is isomorphic to (a, f (a, Fix f)) by means of the constructor C. Therefore, we need to define a function of type

(a, Fix f) -> (a, f (a, Fix f))

By the universal property of product, any such function is necessarily of the form u &&& v for uniquely determined

u :: (a, Fix f) -> a

and

v :: (a, Fix f) -> f (a, Fix f)

There is an obvious candidate for u: the function fst (and, in fact, because we are after a polymorphic u, this is the only choice we have). Is there also a natural choice of v? The answer is yes, and the fundamental reason for that is that Haskell functors are strong. That is, an arbitrary functor f admits the following natural transformation, which in category theory is called the right tensorial strength:

> strength :: Functor f => (a, f b) -> f (a, b)
> strength (x, fy) = fmap (x,) fy

This allows us to define

> fix2cofree' :: Functor f => (a, Fix f) -> Fix ((,) a :. f)
> fix2cofree' = ana (C . (fst &&& strength . second unFix))

free2fix

The initiality of Fix (Either a :. f) implies that each function

(Either a :. f) (Either a (Fix f)) -> Either a (Fix f)

gives rise to a function

Fix (Either a :. f) -> Either a (Fix f)

Therefore, in order to construct a function of the latter type it suffices to come up with a function of the former type.

The type (Either a :. f) (Either a (Fix f)) is isomorphic to Either a (f (Either a (Fix f))) by means of C, therefore we are after a function of type

Either a (f (Either a (Fix f))) -> Either a (Fix f)

By the universal property of sum, any such function is necessarily of the form p ||| q with uniquely determined

p :: a -> Either a (Fix f)

and

q :: f (Either a (Fix f)) -> Either a (Fix f)

We have an obvious candidate for p: the function Left (and because p has to be polymorphic, this is the only choice we have). By analogy with the previous case, we might expect that there always exists a natural transformation of type

Functor f => f (Either a b) -> Either a (f b)

Alas, this is not the case. There is, however, a large class of functors that do admit a natural transformation of this type: Traversable functors, and the required function is sequence.

Therefore, for Traversable functors we can define

> free2fix' :: Traversable f => Fix (Either a :. f) -> Either a (Fix f)
> free2fix' = cata ((Left ||| (right Fix . sequence)) . unC)

Summary

The short answer to Ben’s question is this: fix2cofree works for any functor because all functors in Haskell are strong: for each functor f, there is a natural transformation strength :: Functor f => (a, f b) -> f (a, b), called the right tensorial strength, subject to coherence axioms.

The fundamental fact underlying the existence of strength is that, categorically, every Haskell functor is enriched: its action on morphisms is given not merely as a map from the set of functions a -> b to the set of functions f a -> f b, but as a morphism (in the category Hask) from the internal object of morphisms from a to b, the type a -> b, to the internal object of morphisms from f a to f b, the type f a -> f b. This morphism is fmap, of course. There is a one-to-one correspondence between enrichments of a functor F from a cartesian closed category \mathcal{C} to itself and right tensorial strengths on F. For more information on strong functors, see this nLab web page, or refer to the original paper by Anders Kock.

On the other hand, not every Haskell functor f admits a dual natural transformation Functor f => f (Either a b) -> Either a (f b). Traversable functors do, but the former condition is weaker, I think.

Update: User sclv on reddit suggested that (up to the order of summands) the function f (Either a b) -> Either a (f b) is called costrength in Edward Kmett’s post.