understanding Monoids using F#

A Monoid is one of the most basic algebraic structures that has many instances and applications in computer science and (functional) programming.

And despite it’s scary mathy name it’s really easy to grasp and you are using them already!

first example

A typical example of a Monoid for functional programmers are lists over some type. Those are the elements of our monoid – but we need more:

  • binary operation: the concatenation of two lists will do (it’s @ in F#)
  • neutral element: the empty list.

We are programmers so let’s warp this into a record:

type Monoid<'a> =
        neutral : 'a
        op      : 'a -> 'a -> 'a

module Examples=
    let listM<'l> : Monoid<List<'l>> =
            neutral = []
            op      = fun a b -> a @ b

Definition and Axioms

Of course it is math so there is a formal definition:

A Monoid \( (M, \cdot) \) is a set \(M\) equipped with a binary operation: \( \cdot : M \times M \rightarrow M \) that satisfies the following axioms:

  • the operation is associative. For each \(a\), \(b\) and \(c\) we can choose from \(M\) the following holds: $$( a \cdot b ) \cdot c = a \cdot (b \cdot c)$$
  • there is a neutral Element \(\mathbf{e} \in M\): For each \(a \in M\) $$ \mathbf{e} \cdot a = a \cdot \mathbf{e} = a $$.

Let’s use FsCheck to see if we can find any issues with those Axioms and our lists:

module ``check Monoid axioms`` =
    type T   = List<int>
    let  M   = Examples.listM<int>
    let  Z   = M.neutral
    let (++) = M.op

    let ``Z is the neutral element``(v : T) =
        Z ++ v = v && v ++ Z = v

    let ``the operation is commutative``(a : T, b : T, c : T) =
        a ++ (b ++ c) = (a ++ b) ++ c

The way I prepared this will make it easy to check other instances for us later – we just have to change the definition T and M at the beginning of the module.

Sure enough all tests passes but for list we can really be sure:

a List is a monoid (proof)


You can skip this if you want – it will not help you gain insight into Monoids – see it as a bonus.

So let’s proof the axioms but for this we need to know how @ is implemented. To demonstrate this let’s say it’s implemented like this:

let rec concat (ls : 'a list) (ls' : 'a list) =
    match ls with
    | []      -> ls'
    | (l::ls) -> l :: concat ls ls'

Now the proof is just an exercise in equational reasonings.

Neutral element

Let’s start with the axiom concerning the neutral element: For every list ls we have

[] ++ ls 
= concat [] ls
{ first case in concat }
= ls

So this is easy. For the other case we check ls using structural induction:

For ls = [] it’s again the first case in concat:

ls ++ []
= concat [] []
= [] (== ls)

And for ls = l :: ls' we can argue like this:

ls ++ []
= concat (l:ls') []
{ second case }
= l :: concat ls' []
{ induction }
= l :: ls'
= ls

And we see that [] indeed satisfies this axiom.


For the other axiom again using induction on the first list:

If xs and ys are any lists and if ls = [] then if we compare the left-side of the axiom:

[] ++ (xs ++ ys)
{ we just saw }
= xs ++ ys

with it’s right-side

([] ++ xs) ++ ys
{ using the other axiom again }
= (xs) ++ ys
= xs ++ ys

we see that they match.

Now if ls = l::ls' then:

The left-side is

(ls ++ xs) ++ ys
= ( (l::ls') ++ xs ) ++ ys
{ second case of concat }
= (l :: (ls' ++ xs) ) ++ ys
{ second case of concat }
= l :: ( (ls' ++ xs) ++ ys )
{ induction }
= l :: (ls' ++ (xs ++ ys) )
{ second case of concat in the other direction }
= (l::ls') ++ (xs ++ ys)
= ls ++ (xs ++ ys)

and the last line is just the right side.

This concludes our little proof.

more examples

Of course there are many examples for monoids:

  • integers, addition and 0 as the neutral element:
let intPlus : Monoid<int> =
        neutral = 0I
        op      = (+)
  • integers, multiplication and 1 as the netural element:
let intMult : Monoid<int> =
        neutral = 1
        op      = (*)
  • booleans, conjuction (&&) and true as the neutral element:
let binCon : Monoid<bool> =
        neutral = true
        op      = (&&)
  • functions from a type to itself with composition and id as it’s neutral element:
let funs<'a> : Monoid<'a -> 'a> =
        neutral = id
        op      = (>>)


  • Check that intPlus and intMult are indeed Monoids (use the FsCheck-properties or as a bonus eq. reasoning – hint: better ignore overflows if you want to keep sane)
  • Check binCon – can you find another Monoid using booleans as it’s set?
  • Can you rewrite the FsCheck-properties to show that funs is a Monoid?
  • Strings and string-concatenation form a monoid too but there is something fishy with .net-strings here – can you see it? (Hint: FsCheck will help you out if not) – How can you fix this?

free monoids (bonus)

Free objects are a big deal in category theory and mathematics in general and I only want to mention it here as we’ve already seen the free Monoid in disguise – the list-monoid from the very beginning.

In a sense free just means that it contains all there is to know about monoids: if M is another monoid over the type 't then there is a simple monoid-homomorphism between M and listM<'t>:

let rec hom (M : Monoid<'t>) : ('t list -> 't) =
    | []      -> M.neutral
    | (t::ts) -> M.op t (hom M ts) 

If you look really carefully this is just a fold and if you want you can allow an additional map to get into other monoids as well:

let hom (M : Monoid<'m>) 
        (f : 'l -> 'm) 
        (ls : 'l list)
        : 'm =
    List.foldBack (f >> M.op) ls M.neutral

If you follow this path it will lead you to Haskells Foldable and MapReduce (to a certain extent).