Free.md

Finally Free

{-# LANGUAGE RankNTypes, DeriveFunctor, TypeOperators, KindSignatures, GADTs, DataKinds, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
import Control.Applicative
import Data.Semigroup(Semigroup(..))

If you've programmed in Haskell you may have come across free construcions: free monoids, free monads, free applicatives and so on. But what does it actually mean for an object to be "free"?

The word free has a precise sense in mathematics. Let us look at this typical definition definition from nLab:

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 (known as Type in Haskell for historical reasons).

The functor U is called forgetful because it removes structure. Forgetful and free functors are each others adjoints. The idea behind free constructions is that we can employ unstructured things (such sets) to get structured things (such as a monoids) for free.

For example, consider a forgetful functor from Monoid -> Set and some type/set A. Applying the above definition (and translating it to Haskell syntax), we can see that 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 has the following type signature:

data FreeMonoid a :: Type
instance Semigrup (FreeMonoid a)
instance Monoid (FreeMonoid a)

inject         :: a -> FreeMonoid a
foldFreeMonoid :: Monoid m => (a -> m) -> FreeMonoid a -> m

and must satisfy the law:

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. What we don't know is the actual structure of FreeMonoid. 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.

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

instance Semigroup (FreeMonoid a) where
  FreeMonoid a <> FreeMonoid b = FreeMonoid (liftA2 mappend 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 that foldFreeMonoid does nothing but unwrap the newtype wrapper (the flip is for aesthetical reasons only, we could just as well have defined the type signature as FreeMonoid a -> (a -> m) -> m). We can easily prove 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.

Let's try this with a different structure. What about a group?

class Monoid a => Group a where
  inv :: a -> a

newtype FreeGroup a
  = FreeGroup (forall m . Group m => (a -> m) -> m)

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

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

instance Group (FreeGroup a) where
  inv (FreeGroup a) = FreeGroup (fmap inv a)

injectG :: a -> FreeGroup a
injectG x = FreeGroup (\g -> g x)

foldFreeGroup :: Group m => (a -> m) -> FreeGroup a -> m
foldFreeGroup = flip getFreeGroup
  where
    getFreeGroup (FreeGroup x) = x

This is a valid encoding of a free group in Haskell.

Exercise: come up with an alternative implementation of free groups and show that it is ismorphic to this one.

Higher kinds

So far we have worked on functors from some category to Set. We can also operate on other categories such as the functor category [Set,Set], which allow us to embed structures such as 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) 
instance Applicative (FreeMonad a)
instance Monad (FreeMonad a)

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 our previous encodings, 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 (in Control.Monad.Free). Exercise: write the isorphism.

Libraries

The Haskell community have come up with many encodings of free structures. This table provides an overview some commonly used ones:

Structure	Kind	Free object	η	fold
Semigroup	Type	NonEmpty a	pure	foldMap1
Monoid	Type	[a]	pure	foldMap
Boolean algebra	Type	FreeBoolean a	liftBoolean	foldBoolean
Applicative	Type -> Type	Ap f	liftAp	runAp
Alternative	Type -> Type	Alt f	liftAlt	runAlt
Monad	Type -> Type	Free f	lift	foldFree
Arrow	Type -> Type -> Type	Arr	effect	eval

Other operations

As we alluded to before, the free structures are defined by their fold, with the η acting as an identity. We can define more operations in terms for those. For example:

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

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

For the Type -> Type kind, it looks like this:

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

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

I'm using the names from Control.Monad.Free here, but we should now see that retract and hoist are higher-kinded versions of concat and map respectively.