Some fleeting thoughts I have about `Free` and `Cofree`

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