Free, Finally

Most Haskell programmers have come across the term “free”, often used in conjuction with “monad”, “monoid”, “algebra”. Though I never had a problem understanding these concepts in isolation, it was not entirely clear to me how they related to their definition in category theory.

Given a forgeful functor U : C -> D an object x ∈ D, we define a free C-object on x as an object y ∈ C and a morphism η : x -> U y in D such that for any z ∈ C and f : x -> U z, there exists a unique g : y -> z such that U g ∘ η = f.

Normally we will pick our C to be a category of some algebraic structure such as monoids, groups etc, and D to be Set (or as we like to call it in Haskell: Type). Intuitively U is forgetful because it removes struture from a set. For example, consider a forgetful functor from Monoid -> Type. A free monoid on a consists of a monoidal type FreeMonoid a together with a morphism inject :: a -> FreeMonoid a such that for any other monoidal type m and function f :: a -> m, there exists a unique function g :: FreeMonoid a -> m such that g . inject = f.

In other words, our FreeMonoid is a type constructor with the following operations:

data FreeMonoid a :: Type
instance Semigrup (FreeMonoid a)
instance Monoid (FreeMonoid a)
inject         :: a -> FreeMonoid a
foldFreeMonoid :: Monoid m => (a -> m) -> FreeMonoid a -> m

such that

f = foldFreeMonoid f . inject

Here our foldFreeMonoid is the function that provides the universal mapping from f :: a -> m to g :: FreeMonoid a -> m. We now know the type, functions and what laws to satisfy, but what about the implementation? It turns out we can employ a trick: as FreeMonoid is completely described by the foldFreeMonoid function, we can use it as the definition of the type. This is called a final encoding. We can now define inject and the Monoid instance in a mechanical fashion (we also need to add the superclasses of Monoid).

newtype FreeMonoid a
  = FreeMonoid (forall m . Monoid m => (a -> m) -> m)

instance Semigroup (FreeMonoid a) where
  FreeMonoid a <> FreeMonoid b = FreeMonoid (liftA2 (<>) a b)

instance Monoid (FreeMonoid a) where
  mempty = FreeMonoid (pure mempty)

inject :: a -> FreeMonoid a
inject x = FreeMonoid (\g -> g x)

foldFreeMonoid :: Monoid m => (a -> m) -> FreeMonoid a -> m
foldFreeMonoid = flip getFreeMonoid
  where
    getFreeMonoid (FreeMonoid x) = x

Note we have to flip getFreeMonoid to obtain the signature from the the original definition. We can easily see that the commutativity condition holds.

foldFreeMonoid f . inject = f
(\g -> g x) f             = f x
f x                       = f x

You might have heard that the list is the free monoid in Haskell. The universal property tells us that any free C must be isomorphic to any other free C, so we can prove that [a] is indeed the free monoid on a by witnessing forall a . Iso [a] (FreeMonoid a). This turn out to be trivial:

fmIsList :: (FreeMonoid a -> [a], [a] -> FreeMonoid a)
fmIsList = (toList, fromList)
  where
    toList f = foldFreeMonoid pure
    fromList = Data.Foldable.foldMap inject

Looking back at the types, we can see that inject corresponds to pure and foldFreeMonoid to foldMap. As shown by the isomorphism, we could take an arbitrary function on lists and implement it for our FreeMonoid as well. This suggests a general technique for discovering free structures in Haskell: write the final encoding (a mechanical task) then find a type that is isomorphic to it.

Adding higher kinds #

So far we have worked on functors from some category to Type. We can also operate on other categories such as the functor category Type -> Type, which allow us to embed e.g. monads and applicatives.

type f ~> g = forall a . f a -> g a

newtype FreeMonad f a
  = FreeMonad (forall m . Monad m => (f ~> m) -> m a)

instance Functor (FreeMonad a) where
  fmap f (FreeMonad x) = FreeMonad (\g -> f <$> g x)
instance Applicative (FreeMonad a) where
  pure x = FreeMonad (\_ -> pure x)
instance Monad (FreeMonad a) where

lift :: f ~> FreeMonad f
lift x = FreeMonad (\g -> g x)

foldFree :: Monad m => (f ~> m) -> FreeMonad f ~> m
foldFree f (FreeMonad x) = x f

This is similar to the previous encoding, except we now work with functors and natural transformations rather than values and functors. As before we have an isomorphism between the final encoding and the conventional implementation.

The following table provides an overview of some commonly used encodings.

Ad-hoc operations #

As we alluded to before, the free structures are defined by their fold, with the η acting as an identity. We can also define some commoly used operators.

concat :: Monoid a => FreeMonoid a -> a
concat = foldFreeMonoid id

map :: (a -> b) -> FreeMonoid a -> FreeMonoid b
map f = foldFreeMonoid (inject . f)

retract :: Monad m => Free f ~> f
retract :: foldFree id

hoistFree :: (f ~> g) -> Free f -> Free g
hoistFree f = foldFree (lift . f)

Again, we can see the type signatures and implementations lining up perfectly. In other words, we can think about retract and hoist as higher-kinded versions of concat and map.

Further reading #

• https://peddie.github.io/encodings/encodings-text.html
• https://github.com/aherrmann/final-encoding-examples/tree/master/src
• https://math.stackexchange.com/questions/131389/what-are-free-objects
• https://math.stackexchange.com/questions/131389/what-are-free-objects