Some fleeting thoughts I have about Free and Cofree…

Table of Contents⌗

Introduction⌗

I recently tweeted that:

I like to think of Free and Cofree in terms of combinators.

Free f a makes it easy to use f as a fixed point, by having the choice of either termination or recursion.

Cofree f a does the same in terms of recursion, albeit without the termination.

As it turns out, I was pretty close to an intuitive definition.

Cofree is the dual of Free⌗

“Co-” is typically used as a prefix to denote the categorical dual of some concept. For example, coproduct (read: sum) types are the categorical dual of product types. Similarly, the convention can also be observed in Monad and Comonad.

The duality of Free and Cofree can be observed without taking into account their roots in category theory. Free is encoded using a sum type—on the other hand, Cofree is encoded using a product type.

data Free f a = Pure a | Roll (f (Free f a))

data Cofree f a = CofreeCons a (f (Cofree f a)

If this isn’t convincing from a practical standpoint, take a look at how Free and Cofree is folded and unfolded respectively. If you squint hard enough, you can see the signatures for the cata and ana recursion schemes, which they themselves are duals.

runFree :: forall f a. Functor f => (f (Free f a) -> Free f a) -> Free f a -> a

cata :: forall f a. (f a -> a) -> Mu f -> a

buildCofree :: forall f s a. Functor f => (s -> Tuple a (f s)) -> s -> Cofree f a

ana :: forall f a. (a -> f a) -> a -> Mu f

This puts into mind the duality of recursion and corecursion. Recursion involves folding compounded data into a base case, while corecursion involves unfolding a seed into compounded data. In the same vein, Free f and Cofree f can be treated as combinators that provide the least and greatest fixed point of f respectively. This is discussed in the following section.

Deriving Mu f⌗

In PureScript, Mu f is a type which provides the least fixed point of some functor f. It essentially allows the construction of recursive data types without any form of self-reference, similar to how the fix function at the term-level allows recursion in a lambda. That said, type f type is responsible for providing a base case such that a finite Mu f can be built.

newtype Mu f = In (f (Mu f))

Using Free f Void⌗

Mu f can be derived from Free by making the Pure constructor impossible to use. This can be achieved through the use of Void, which has no constructors and as such, cannot exist at the term-level.

Free f Void = Pure Void | Roll (f (Free f Void))

Free f Void = Roll (f (Free f Void))

Using Cofree f Unit⌗

Mu f can be derived from Cofree by making the head in CofreeCons to always be inhabited by a single value. This can be achieved through the use of Unit, which always has a single constructor and as such, can be eliminated from the constructor.

Cofree f Unit = CofreeCons Unit (f (Cofree f Unit))

Cofree f Unit = CofreeCons (f (Cofree f Unit))

Cofree in Practice⌗

To motivate the use of Cofree, here are a few examples that I’ve synthesized. I’m not discussing Free here as its primary use-case of turning regular functors into monads warrants its own post.

Cofree as an infinite stream⌗

Cofree Id a encodes an infinite stream of values of type a. The stream is built using buildCofree and a coalgebra describing how the seed can synthesize a return value as well as another seed which will be used in the future. This is a practical example of corecursion: we’re not moving towards a base case nor do we have the option to terminate.

module Main where

import Prelude

import Control.Comonad.Cofree (Cofree, buildCofree, head, tail)
import Data.Tuple (Tuple(..))
import Effect (Effect)
import Effect.Console (logShow)
import Data.Functor.Polynomial (Id(..))

factorial_ :: Cofree Id Int
factorial_ = buildCofree coal seed
  where
  seed :: Tuple Int Int
  seed = Tuple 0 1

  coal :: Tuple Int Int -> Tuple Int (Id (Tuple Int Int))
  coal (Tuple n f) = Tuple f (Id (Tuple (n + 1) (f * (n + 1))))

factorial :: Int -> Int
factorial = flip go factorial_
  where
  go 0 = head
  go n = tail >>> case _ of
    Id co -> go (n - 1) co

main :: Effect Unit
main = do
  logShow $ factorial 5