# Free and Cofree

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
```