Some fleeting thoughts I have about
Table of Contents⌗
Cofreeis the dual of
- Cofree in Practice
I recently tweeted that:
I like to think of
Cofreein terms of combinators.
Free f amakes it easy to use
fas a fixed point, by having the choice of either termination or recursion.
Cofree f adoes 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
“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
The duality of
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
Cofree is folded and unfolded respectively. If you squint hard enough, you can see the signatures for the
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.
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))
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))
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