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 -> Dan object
x ∈ D, we define a free
xas an object
y ∈ Cand a morphism
η : x -> U yin D such that for any
z ∈ Cand
f : x -> U z, there exists a unique
g : y -> zsuch 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:
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
f = foldFreeMonoid f . inject
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
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
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.
|Boolean algebra||Type||FreeBoolean a||liftBoolean||foldBoolean|
|Alternative||Type -> Type||Alt f||liftAlt||runAlt|
|Applicative||Type -> Type||Ap f||liftAp||runAp|
|Monad||Type -> Type||Free f||lift||foldFree|
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
hoist as higher-kinded versions of