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
andCofree
in terms of combinators.
Free f a
makes it easy to usef
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