### Category Theory Helpline

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 from a cartesian closed category to itself and right tensorial strengths on . 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.