Given a set , the free monoid on is the set of all lists (finite sequences) of elements of , made into a monoid using concatenation. The free functor from Set to Mon? takes to .
We will give three definitions, which can all be shown equivalent.
An element of consists of a natural number (possibly ) and function from to , where is the subset of . Such an element is called a list or (to specify ) -tuple of elements of . The number is called the length of the list.
The empty list is the unique list of length . It may be written , , or , perhaps with a subscript if desired.
If , then the list which assigns to may be written . For example, if are elements of , then is an element of .
Given two lists and , the former of length and the latter of length , their concatenation is a list of length , given as follows:
One can now show that concatenation is associative with the empty list as identity; hence is a monoid.
The (underlying) set may be defined as an inductive type? as follows. There are two basic constructors, one with no arguments, and one with two arguments, of which one is an element of and the other is an element of . By the yoga of inductive types, that is a complete definition, but we spell it out in more detail while also giving terminology and notation.
So, a list is either the empty list or the cons (short for ‘constructor’ and deriving from Lisp) of an element of and a (previously constructed) list . The empty list may may be written , , or , perhaps with a subscript if desired; the cons of and may be written , , or . We interpret the definition recursively?, so we can list the elements of in the order in which they appear:
* ,
Here, are elements of . We may continue the ‘etc’ as far as we like, but no farther; while there are lists of arbitrarily long finite length, there are no lists of infinite length. (We would get such lists, however, if we interpreted the definition corecursively.) We normally abbreviate the lists above as follows: * ,
We still must define the monoidal structure on ; we define the concatenation of and recursively in . To be explicit:
One can now show that concatenation is associative with the empty list as identity; hence is a monoid.
In the course of proving that the category Mon? of monoids is a complete category, one normally shows that the forgetful functor (from to the category Set of sets) preserves all limits. Thus, the adjoint functor theorem defines a left adjoint to if a size condition is met; this adjoint is the functor that takes a set to its free monoid .
To be sure, meeting the solution set condition basically requires starting the constructions in one of the other definitions above; but the proofs may all be thrown onto the adjoint functor theorem.
If the free moniod functor is followed by the forgetful functor , then we get a monad on . This monad is very important in computer science, where it is known as the list monad.
The list monad bears the same relation to multicategories as the identity monad on bears to ordinary categories. This relation should be explained at generalized multicategory.
Every definition of free monoid makes use of some form of axiom of infinity, either directly or the ability form general inductive types. Indeed, as , the axiom of infnity follows from the existence of free monoids.