The fixed point functors of Free and Cofree

Question

To make that clear, I'm not talking about how the free monad looks a lot like a fixpoint combinator applied to a functor, i.e. how Free f is basically a fixed point of f. (Not that this isn't interesting!)

What I'm talking about are fixpoints of Free, Cofree :: (*->*) -> (*->*), i.e. functors f such that Free f is isomorphic to f itself.

Background: today, to firm up my rather lacking grasp on free monads, I decided to just write a few of them out for different simple functors, both for Free and for Cofree and see what better-known [co]monads they'd be isomorphic to. What intrigued me particularly was the discovery that Cofree Empty is isomorphic to Empty (meaning, Const Void, the functor that maps any type to the uninhabited). Ok, perhaps this is just stupid – I've discovered that if you put empty garbage in you get empty garbage out, yeah! – but hey, this is category theory, where whole universes rise up from seeming trivialities... right?

The immediate question is, if Cofree has such a fixed point, what about Free? Well, it certainly can't be Empty as that's not a monad. The quick suspect would be something nearby like Const () or Identity, but no:

Free (Const ()) ~~ Either () ~~ Maybe
Free Identity   ~~ (Nat,)    ~~ Writer Nat

Indeed, the fact that Free always adds an extra constructor suggests that the structure of any functor that's a fixed point would have to be already infinite. But it seems odd that, if Cofree has such a simple fixed point, Free should only have a much more complex one (like the fix-by-construction FixFree a = C (Free FixFree a) that Reid Barton brings up in the comments).

Is the boring truth just that Free has no “accidental fixed point” and it's a mere coincidence that Cofree has one, or am I missing something?

Answer 1

Since you asked about the structure of the fixed points of Free, I'm going to sketch an informal argument that Free only has one fixed point which is a Functor, namely the type

newtype FixFree a = C (Free FixFree a)

that Reid Barton described. Indeed, I make a somewhat stronger claim. Let's start with a few pieces:

newtype Fix f a = Fix (f (Fix f) a)
instance Functor (f (Fix f)) => Functor (Fix f) where
  fmap f (Fix x) = Fix (fmap f x)

-- This is basically `MFunctor` from `Control.Monad.Morph`
class FFunctor (g :: (* -> *) -> * -> *) where
  hoistF :: Functor f => (forall a . f a -> f' a) -> g f b -> g f' b

Notably,

instance FFunctor Free where
  hoistF _f (Pure a) = Pure a
  hoistF f (Free fffa) = Free . f . fmap (hoistF f) $ fffa

Then

fToFixG :: (Functor f, FFunctor g) => (forall a . f a -> g f a) -> f a -> Fix g a
fToFixG fToG fa = Fix $ hoistF (fToFixG fToG) $ fToG fa

fixGToF :: forall f b (g :: (* -> *) -> * -> *) .
           (FFunctor g, Functor (g (Fix g)))
        => (forall a . g f a -> f a) -> Fix g b -> f b
fixGToF gToF (Fix ga) = gToF $ hoistF (fixGToF gToF) ga

If I'm not mistaken (which I could be), passing each side of an isomorphism between f and g f to each of these functions will yield each side of an isomorphism between f and Fix g. Substituting Free for g will demonstrate the claim. This argument is very hand-wavey, of course, because Haskell is inconsistent.

Answer 2

Your observation that Empty is a fixed point of Cofree (which is not really true in Haskell, but I guess you want to work in some model that ignores ⊥, like Set) boils down to the fact that

there is a set E (the empty set) such that for every set X, the projection p₂ : X × E -> E is an isomorphism.

We could say in this situation that E is an absorbing object for the product. We can replace the word “set” by “object of C” for any category C with products, and we get a statement about C that may or may not be true. For Set, it happens to be true.

If we pick C = Set^op, which also has products (because Set has coproducts), and then dualize the language to talk about sets again, we get the statement

there is a set F such that for every set Y, the inclusion i₂ : F -> Y + F is an isomorphism.

Obviously, this statement is not true for any set F (we can pick any non-empty set Y as a counterexample for any F). No surprise there, after all Set^op is a different category from Set.

So, we won't get a “trivial fixed point” of Free in the same way we got one for Cofree, because Set^op is qualitatively different from Set. The initial object of Set is an absorbing element for the product, but the terminal object of Set is not an absorbing object for the coproduct.

---

If I may get on my soapbox for a moment:

There is much discussion among Haskell programmers about which constructions are the “duals” of which other constructions. Most of this is in a formal sense meaningless, because in category theory dualizing a construction works like this:

Suppose I have a construction which I can perform on any category C (or any category with certain extra structure and/or properties). Then the dual construction on a category C is the original construction on the opposite category C^op (which had better have the extra structure and properties we needed, if any).

For example: The notion of products makes sense in any category C (though products might not always exist), via the universal property defining products. To get a dual notion of coproducts in C we should ask what are the products in C^op, and we have just defined what products are in any category, so this notion makes sense.

The trouble with applying duality to the setting of Haskell is that the Haskell language prefers overwhelmingly to talk about just one category, Hask, in which we do our constructions. This causes two problems for talking about duality:

• To obtain the dual of a construction as described above, I am supposed to be able to be able to do the construction in any category, or at least any category of a particular form. So we must first generalize the construction that, typically, we have only done in the category Hask to a larger class of categories. (And having done so, there are plenty of other interesting categories we could potentially interpret the resulting notion in besides Hask^op, such as Kleisli categories of monads.)

• The category Hask enjoys many special properties which can be summarized by saying that (ignoring ⊥) Hask is a cartesian closed category. For example, this implies that the initial object is an absorbing object for the product. Hask^op does not have these properties, which means that the generalized notion may not make sense in Hask^op; and it can also mean that two notions which happened to be equivalent in Hask are distinct in general, and have different duals.

For an example of the latter, take lenses. In Hask they can be constructed in a number of ways; two ways are in terms of getter/setter pairs and as coalgebras for the costate comonad. The former generalizes to categories with products and the second to categories enriched in a particular way over Hask. If we apply the former construction to Hask^op then we get out prisms, but if we apply the latter construction to Hask^op then we get algebras for the state monad and these are not the same thing.

A more familiar example might be comonads: starting from the Haskell-centric presentation

return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

some insight seems to be needed to determine which arrows to reverse to obtain

extract :: w a -> a
extend :: w a -> (w b -> a) -> w b

The point is that it would have been much easier to start from join :: m (m a) -> m a instead of (>>=); but finding this alternative presentation (equivalent due to special features of Hask) is a creative process, not a mechanical one.

In a question like yours, and many others like it, where it is pretty clear what sense of dual is intended, there's still absolutely no reason to expect a priori that the dual construction will actually exist or have the same properties as the original, because Hask^op qualitatively behaves quite differently from Hask. A slogan might be

the theory of categories is self-dual, but the theory of any particular category is not!