Search code examples
haskellcategory-theoryfree-monadfixpoint-combinators

The fixed point functors of Free and Cofree


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?


Solution

  • 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.