Free structure
Contents
Introduction
This article attempts to give a relatively informal understanding of "free" structures from algebra/category theory, with pointers to some of the formal material for those who desire it.
Algebra
What sort of structures are we talking about?
Free structures originate in abstract algebra, so that provides a good place to start. Some common structures in algebra are:
- Monoids
- consisting of
- A set
- An identity
- A binary operation
- And satisfying the equations
- consisting of
- Groups
- consisting of
- A monoid
- An additional unary operation
- satisfying
- consisting of
- Rings
- consisting of
- A set
- A unary operation
- Two binary operations
- Distinguished elements
- such that
- is a group
- is a monoid
- consisting of
So, for algebraic structures, we have sets equipped with operations that are expected to satisfy equational laws.
Free algebraic structures
Now, given such a description, we can talk about the free structure over a particular set (or, possibly over some other underlying structure; but we'll stick with sets now). What this means is that given , we want to find some set , together with appropriate operations to make the structure in question, along with the following two criteria:
- There is an injection
- The structure generated is as 'simple' as possible.
- should contain only elements that are required to exist by and the operations of the structure.
- The only equational laws that should hold for the generated structure are those that are required to hold by the equational laws for the structure.
So, in the case of a free monoid (from here on out, we'll assume that the structure in question is a monoid, since it's simplest), the equation should not hold unless , or .
For monoids, the free structure over a set is given by the monoid of lists of elements of that set, with concatenation as multiplication. It should be easy to convince yourself of the following (in pseudo-Haskell):
M = [S]
e = []
* = (++)
i : S -> [S]
i x = [x] -- i x = x : []
[] ++ xs = xs = xs ++ []
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
xs ++ ys = ys ++ xs iff xs == ys || xs == [] || ys == []
-- etc.
The category connection
Free structure functors
One possible objection to the above description (even a more formal version thereof) is that the characterization of "simple" is somewhat vague. Category theory gives a somewhat better solution. Generally, structures-over-a-set will form a category, with arrows being structure-preserving homomorphisms. "Simplest" (in the sense we want) structures in that category will then either be initial or terminal, and thus, freeness can be defined in terms of such universal constructions.
In its full categorical generality, freeness isn't necessarily categorized by underlying set structure, either. Instead, one looks at "forgetful" functors from the category of structures to some other category. For our free monoids above, it'd be:
The functor taking monoids to their underlying set. Then, the relevant universal property is given by finding an adjoint functor:
- , ⊣
being the functor taking sets to the free monoids over those sets. So, free structure functors are left adjoint to forgetful functors. It turns out this categorical presentation also has a dual: cofree structure functors are right adjoint to forgetful functors.
Algebraic constructions in a category
Category theory also provides a way to extend specifications of algebraic structures to more general categories, which can allow us to extend the above informal understanding to new contexts. For instance, one can talk about monoid objects in an arbitrary monoidal category. Such categories have a tensor product of objects, with a unit object (both of which satisfy various laws).
A monoid object in a monoidal category is then:
- An object
- A unit 'element'
- A multiplication
such that:
Where:
- and are the identity isomorphisms for the monoidal category, and
- is part of the associativity isomorphism of the category.
So, hopefully the connection is clear: we've generalized the carrier set to a carrier object, generalized the operations to morphisms in a category, and equational laws are promoted to being equations about composition of morphisms.
Monads
One example of a class of monoid objects happens to be monads. Given a base category , we have the monoidal category :
- Objects are endofunctors
- Morphisms are natural transformations between the functors
- The tensor product is composition:
- The identity object is the identity functor, , taking objects and morphisms to themselves
If we then specialize the definition of a monoid object to this situation, we get:
- An endofunctor
- A natural transformation
- A natural transformation
which satisfy laws that turn out to be the standard monad laws. So, monads turn out to be monoid objects in the category of endofunctors.
Free Monads
But, what about our intuitive understanding of free monoids above? We wanted to promote an underlying set, but we have switched from sets to functors. So, presumably, a free monad is generated by an underlying (endo)functor, . We then expect there to be a natural transformation , 'injecting' the functor into the monad.
In Haskell, we can write the type of free monads over Haskell endofunctors as follows:
data Free f a = Return a | Roll (f (Free f a))
instance Functor f => Monad (Free f) where
return a = Return a
Return a >>= f = f a
Roll ffa >>= f = Roll $ fmap (>>= f) ffa
-- join (Return fa) = fa
-- join (Roll ffa) = Roll (fmap join ffa)
inj :: Functor f => f a -> Free f a
inj fa = Roll $ fmap Return fa
This should bear some resemblance to free monoids over lists. Return
is analogous to []
, and Roll
is analogous to (:)
. Lists let us create arbitrary length strings of elements from some set, while Free f
lets us create structures involving f
composed with itself an arbitrary number of times (recall, functor composition was the tensor product of our category). Return
gives our type a way to handle the 0-ary composition of f
(as []
is the 0-length string), while Roll
is the way to extend the nesting level by one (just as (:)
lets us create (n+1)-length strings out of n-length ones). Finally, both injections are built in a similar way:
inj_list x = (:) x []
inj_free fx = Roll (fmap Return fx)
This, of course, is not completely rigorous, but it is a nice extension of the informal reasoning we started with.
Further reading
For those looking for an introduction to the necessary category theory used above, Steve Awodey's Category Theory is a popular, freely available reference.