Free structure
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. The later sections make use of some notions from category theory, so some familiarity with its basics will be useful.
Algebra
What sort of structures are we talking about?
The distinction between free structures and other, non-free structures, originates in abstract algebra, so that provides a good place to start. Some common structures considered 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 embedding
- 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 structures of that type.
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 . Further , for all , and , and (and these should all be distinct, except as required by the monoid laws), but there should be no 'extra' elements of in addition to those.
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, [1] 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 [2] 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 [3] 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.
Notes
Universal constructions
Initial (final) objects are those that have a single unique arrow from (to) the object to (from) every other object in the category. For instance, the empty set is initial in the category of sets, and any one-element set is final. Initial objects play an important role in the semantics of algebraic datatypes. For a datatype like:
data T = C1 A B C | C2 D E T
we consider the following:
- A functor ,
- F-algebras which are:
- An object
- An action
- Algebra homomorphisms
- These are given by such that
The datatype T
is then given by an initial F-algebra. This works out nicely because the unique algebra homomorphism whose existence is guaranteed by initiality is the fold or 'catamorphism' for the datatype.
Intuitively, though, the fact that T
is an F-algebra means that it is in some sense closed under forming terms of shape F---suppose we took the simpler signature FX = 1 + X
of the natural numbers; then both Z = inl () and Sx = inr x can be incorporated into Nat. However, there are potentially many algebras; for instance, the naturals modulo some finite number, and successor modulo that number are an algebra for the natural signature.
However, initiality constrains what Nat can be. Consider, for instance, the above modular sets 2 and 3. There can be no homomorphism :
-
- but
-
- but
-
- but
-
This is caused by these algebras identifying elements in incompatible ways (2 makes SSZ = Z, but 3 doesn't, and 3 makes SSSZ = Z, but 2 doesn't). So, the values of an initial algebra must be compatible with any such identification scheme, and this is accomplished by identifying none of the terms in the initial algebra (so that h is free to send each term to an appropriate value in the target, according to the identifications there). A similar phenomenon occurs in the main section of this article, except that the structures in question have additional equational laws that terms must satisfy, so the initial structure is allowed to identify those, but no more than those.
By the same argument, we can determine that 3 is not a final algebra. Nor are the naturals (for any modular set M, S(h(M-1)) = S(M-1) = M, but h(S(M-1)) = h0 = 0). The final algebra is the set {0}, with S0 = 0 and Z = 0, with unique homomorphism hx = 0. This can be seen as identifying as many elements as possible, rather than as few. Naturally, final algebras don't receive that much interest. However, finality is an important property of coalgebras.
Forgetful functors
The term "forgetful functor" has no formal specification; only an intuitive one. The idea is that one starts in some category of structures, and then defines a functor by forgetting part or all of what defines those structures. For instance:
- , where is any category of algebraic structures, and U simply forgets about all of the n-ary operations and equational laws, and takes structures to their underlying sets, and homomorphisms to functions over those sets.
- , which takes a group and forgets about the inverse operation to give a monoid. This functor would then be related to "free groups over a monoid".
Natural transformations
The wiki article gives a formal definition of natural transformations, but a Haskell programmer can think of a natural transformation between functors F and G as:
trans :: forall a. F a -> G a