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?

Meridithmeriel

Of course in Haskell Free must have a fixed point, namely newtype FixFree a = C (Free FixFree a), and FixFree () has lots of values like C (Pure ()), C (Free (C (Pure (Pure ())))) (typed holes were useful here...), and so on. The interesting question would be to understand what the structure of these values is. – Swag

@ReidBarton that's of course one fixpoint, but Cofree has one like that too and it's not Empty. I'm asking about nontrivially trivial fixpoints, not about trivially nontrivial fixpoints, if that makes sense... – Meridithmeriel

It sort of makes sense, but IMO you've made the question much less interesting :) – Swag

Have I? Well, it would certainly be interesting to investigate the constructed fixpoints as well – particularly, if it somehow relates to the fixpoints that I meant. But a separate question about the structure of FixFree and FixCofree might also be appropriate. – Meridithmeriel

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.

Faugh

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!

Swag

To clarify: () in Set^op is not absorbing because () in Set is not only the terminal object but also has outgoing morphisms to any other object (besides Void)? – Excommunicative

I hadn't thought of it in those terms but you're right. What I called an absorbing object for products is the same as a strict initial object (ncatlab.org/nlab/show/strict+initial+object). – Swag

I don't quite get your rant. You are completely correct that it's not a given that a dual construction exists in a category, in the sense that if category C has structure P, then C^op has structure P. But that this isn't true is why such things are discussed so much. If it was true, it would just be taken for granted. It's certainly valuable and interesting to know when some constructions are dual, and it is interesting to imagine what it would mean if certain dual constructions existed. For example, the dual to cartesian closure. A cartesian closed category... – Goahead

...with an initial object that is also "co-cartesian closed" collapses to a preorder. To try to say the "coexponentials" we cast away products and/or coproducts. This is actually more accurate. Haskell does not have categorical coproducts. Using monoidal, or even premonoidal, structure instead allows exponentials and coexponentials to coexist, e.g. Declarative Continuations and Categorical Duality and Control Categories and Duality. – Goahead

@DerekElkins There's no problem with saying "the dual to cartesian closure" because cartesian closure is a property that we can check for any category. The problem is with asking "what is the dual to a -> b?" Depending on the setting, I might want to treat it as the cartesian closed structure, some arbitrary monoidal closed structure, or just a component of a natural transformation. – Swag

Maybe the clearest example of ambiguity is for monoids. I can define monoid objects in any monoidal category. On any category with products I get a Cartesian monoidal structure. That construction is how I define monoids in Hask (or Set). Hask^op also has products so I can use the same construction to define comonoids in Hask; they are comonoids for the coproduct in Hask. On the other hand the opposite of any monoidal category is also monoidal, and if I take monoids in (Hask, x)^op I get comonoids for the product in Hask. Which of these is "the" dual notion to monoids? – Swag

@ReidBarton Okay, it didn't come across to me that your focus was on vagueness and ambiguity. Unfortunately, it's probably a tilting at windmills situation. On one side, many people only have a vague understanding of duality and categorical constructions, and on the other, I can understand people not always wanting to say something like "this is the construction in the co-bicategory of the bicategory of profunctors, not to be confused with the op-bicategory" as opposed to "these constructions are dual in a sense". – Goahead