I'm currently learning abstract algebra and the word free appears (free monoid, free vector space) throughout different literatures. Is there a general (and simple) definition of the word (and possibly examples in functional programming) or is it merely a highly overloaded word? Many Thanks!
Yes, and in fact there is even a general notion of an algebraic theory, and thus algebraic object. An algebraic theory consists of:
- a sort
- constants and function symbols
- algebraic axioms, that is universally quantified sentences which may contain equality, but no other logical symbols (ie. $\exists,\vee,\to,\neg$)
It is worth noting that the theory of fields is not algebraic, thus there are no free fields.
So the theory of monoids $\mathcal M$ has a sort $M$, constant $e : M$, function symbol $\mu:G\times G\to G$, and axioms
- $\forall x.\mu(x,e)=x$
- $\forall x.\mu(e,x)=x$
- $\forall x,y,z.\mu(\mu(x,y),z)=\mu(x,\mu(y,z))$
In general, given an algebraic theory $T$ we may consider the set of terms in this theory. Categorically, a free algebra for $T$ is the initial object in the category of algebras for $T$. The standard way to construct the free algebra is to take the term model for $T$, that is the underlying set of the free algebra is the set of terms of $T$ modulo the equivalence relation generated by the axioms of $T$.
So what we mean by a free structure in the theory $T$ generated by the set $B$, is to consider a free algebra for the theory $T_B$ containing an additional constant symbol for each element of $B$.
This description is concrete but a bit complicated. There is a much simpler but more abstract construction using the theory of monads, because an algebraic theory corresponds precisely to a monad.
An example for monoids in a functional programming language could look as follows, by interpreting the theory of monoids as a monad:
type 'a mon = | Id | Bin of 'a mon * 'a mon | Var of 'a let return (x : 'a) : 'a mon = Var x let rec bind (x : 'a mon) (f : 'a -> 'b mon) : 'b mon = match x with | Id -> Id | Bin (s,t) -> Bin (bind s f, bind t f) | Var u -> f u let rec eq (a_eq : 'a -> 'a -> bool) (s : 'a mon) (t : 'a mon) : bool = match (s,t) with | (Bin (Id,u), v) | (Bin (u,Id), v) | (u, Bin (Id,v)) | (u, Bin (v,Id)) -> eq u v | (Bin (Bin (u1,u2),u3), v) -> eq (Bin u1, Bin (u2,u3)) v | (u, Bin (Bin (v1,v2),v3)) -> eq u (Bin v1, Bin (v2,v3)) | (Id,Id) -> true | (Bin (u1,v1), Bin (u2,v2)) -> (eq u1 u2) && (eq v1 v2) | (Var x, Var y) -> a_eq x y | _ -> false type two = A | B let two_eq x y : bool = match (x,y) with | (A,A) | (B,B) -> true | _ -> false
Then the type
two mon with relation
eq two_eq gives the free monoid on two elements.
return : two -> two mon gives us the two generators
return A and
bind : two mon -> (two -> 'b mon) -> 'b mon tells us that a map from the free monoid on two elements to another (in this case free) monoid is uniquely determined by what the elements of
two are mapped to.