# 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 $
-> do x <- a embed
\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`

?