Initial And Final Free Structures

In this note I show how to construct free structures in Haskell. I show both initial and final structures. I make a brief comparison by example, and point out the relation with some existing implementations. A small generalization is also proposed.

The code presented below is compilable, but you need a few extensions:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UnicodeSyntax #-}

Free monoid

We’ll show how this is done first on the monoid example. It’s simple enough while having sufficient complexity to illustrate most issues.

Initial encoding

The idea of a free construction is to add the operations of a given algebraic structure (in this case, a monad) around a set of generators (which need not exhibit the structure). One way to construct a free structure is to have one constructor for each operation in the structure, plus one to embed generators. This is called the “initial” encoding. For a monoid structure, we would have the following:

data FreeMonoid t where
  Mappend :: FreeMonoid t -> FreeMonoid t -> FreeMonoid t
  Mempty :: FreeMonoid t
  Embed0 :: t -> FreeMonoid t

However the above ignores the associativity law of monoids. For one, it is possible to distinguish objects on the basis of the association structure of Mappend. One way to take into account associativity is to force one particular association. For example, we can force associating on the right. To take care of the unit law, we also won’t allow Mempty on the left of Mappend. Thus, the only thing that we can do on the left of Mempty is embed. We obtain:

data FreeMonoid t where
  Mappend :: t -> FreeMonoid t -> FreeMonoid t
  Mempty :: FreeMonoid t

This is simply the list type. While it is indeed a free monoid, it has some problems, such as an expensive append. To address this issue, one could choose to use the first representation, and simply make sure that no program makes observable identified objects; for example by making the type private (exporting it abstractly) and having an interpretation function fold which does not expose the structure.

Final encoding

Another useful representation of free structures is the so called “final” one. Essentially, it is a church-encoded version of the “initial” encoding. Let’s review quickly Church encodings. If a data type can be written as the fixpoint of some functor f:

data Fix f = In (f (Fix f))

then its Church encoding is as follows:

type Church f = ∀α. (f α → α) → α

For our first version of the free monoid, the functor in question is (exercise):

F t α = (α × α) + α + t

We an now compute Church F by distributing the sum over the function type, using the isomorphism (a + b) → c = (a → c) × (b → c):

Church F = (((α × α) + α + t) → α) → α
         = (((α × α) → α) × (α → α) × (t → α)) → α

We have here a tuple with three components. The first two components are the types of mappend and mempty, and the last one corresponds to the embedding function. Therefore, if we wish, we can substitute the first two components by a constraint that α has a monoid structure.

Church F = (Monoid α × (t → α)) → α

Going back to Haskell:

newtype FreeMonoidFinal t = MF (forall a. Monoid a => (t → a) → a)

One advantage of this formulation is that we do not have to worry about laws any more. Rather, we pass the buck to the Monoid a instance. If it satisfies the laws, then our encoding will automatically satisfy them as well. Consequently, we can even generalise the above free construction to any structure represented as a Haskell class, thanks to the support of GHC for abstracting over constraints:

newtype Free0 k t = Free0 (forall a. k a => (t → a) → a)

Before closing this section, let’s make sure we did not delude ourselves by providing the appropriate instances:

instance Semigroup (Free0 Monoid t) where
  (MF f) <> (MF g) = MF (\embed -> f embed <> g embed)
instance Monoid (Free0 Monoid t) where
  mempty = MF (\_ -> mempty)

Free Monad

Initial encoding

We can now repeat the same steps for monad instead of monoid.

The naive initial encoding is as follows:

data FreeMonadInitial t a where
  Embed1 :: t a -> FreeMonadInitial t a
  Return :: a -> FreeMonadInitial t a
  Bind :: FreeMonadInitial t a -> (a -> FreeMonadInitial t b) -> FreeMonadInitial t b

The right-associated one looks like this (on the left of bind we allow only to embed):

data FreeMonad' t a where
  Return' :: a -> FreeMonad' t a
  BindEmbed :: t a -> (a -> FreeMonad' t b) -> FreeMonad' t b

The above version is derived by Kiselyov and Iishi in “Freer Monads, More Extensible Effects”, in a different way than mine.

Instead of a presentation based on bind, there is another presentation of monads, based on join : m (m a) → m a. As far as I know this is the leading presentation in category theory. It makes in particular more plain that a monad is a monoid (join is like mappend) in the suitable category (endofunctors).

If we are to construct our free structure using join instead of bind, then we find this definition:

data FreeMonad'' t a where
  Embed :: t a -> FreeMonad'' t a
  Join :: FreeMonad'' t (FreeMonad'' t a) -> FreeMonad'' t a
  Pure :: a -> FreeMonad'' t a

The above version also ignores the laws. But as before, we can repair this issue by changing the Join constructor, so that it refers to t directly instead of FreeMonad'' t in the left (of the functor composition):

data FreeMonad'' t a where
  JoinEmbed :: t (FreeMonad'' t a) -> FreeMonad'' t a
  Pure :: a -> FreeMonad'' t a

This is the version proposed by Kmett in one of his library and has been the basis of many applications.

Final encoding

To construct the final representation of a free monad, let’s instead adapt the generic free structure of arity 0, to arity 1. Essentially, it suffices to add type parameters where they are necessary. (One trap is that there must be inner quantification.)

newtype Free1 k t x = Free1 (forall a. k a => (forall x. t x → a x) → a x)

Just to make sure, let’s check we made no mistake by defining the monad instance for Free1 Monad t

instance Functor (Free1 Monad t) where
  fmap f (Free1 x)  = Free1 (\embed -> fmap f (x embed))

instance Applicative (Free1 Monad t) where
  pure x = Free1 (\embed -> pure x)
  Free1 f <*> Free1 g = Free1 (\embed -> f embed <*> g embed)

instance Monad (Free1 Monad t) where
  Free1 a >>= f = Free1 $
    \embed -> do x <- a embed
                 let Free1 b = f x
                 b embed

(All these instances can be defined in a completely systematic way. Perhaps an idea for a future GHC extension?)

Free anything

We above final encoding is easy to generalise to any arity. Here it is for 2:

newtype Free2 k t x y =
   Free2 (forall a. k a => (forall x y. t x y → a x y) → a x y)

This way we can have Free2 Category, Free2 Arrow, etc.

As an exercise, can you find applications for those? What about Free0 Ring or Free1 Traversable?