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

    [<Property>]
    let ``Z is the neutral element``(v : T) =
        Z ++ v = v && v ++ Z = v

    [<Property>]
    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)


remark

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.

Associativity

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      = (>>)
    }

exercises

  • 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) =
    function
    | []      -> 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).

  • Pingback: Dew Drop – March 4, 2015 (#1967) | Morning Dew()

  • Colin A

    Does the .NET strings exercise have something to do with the string class not acting kindly with concatenation for all possible states that strings can be in?

    Another great blog post! A more general question that you probably can’t answer succinctly, but perhaps can give me a clue towards. What do monoids get you? Why are they so good?

    Fond Regards,
    Colin

    • To the first: yes – there is basically another neutral element that is not equal to the empty string (under the String.Equals)

      Monoids as is does not give you much for your daily work (especially as there is no *nice* way to abstract over all of them in F#s type-system).

      It’s more like a pattern in OOP – you can talk about the concept and everyone knows what you mean and you might hear about them from time to time (google for Monads – you might find cups, t-shirts, posters, etc. mentioning monoids ;))

      But overall you will do fine as a F# programmer without caring a bit about this stuff – but it will not hurt you either.

    • John Azariah

      Monoids basically give you the ability to parallelise the operation over the set – this is a direct consequence of the fact that the operation is associative and closed, so the order in which you perform the operation doesn’t matter…

      Think of it as a design pattern that allows you to quickly perform “fold” (or “reduce”, specifically) on a collection of your type in a parallel way without extra effort, because the mathematics under it supports you to do that!

      • Colin A

        Thanks for the reply John! I was wonder though… how can you perform a reduce in parallel? Doesn’t each fold require two operands? Do you do it like a merge sort or something (in terms of when you can apply whatever function you are using to fold)? I feel like the answer might be something something currying, but you won’t know what you should apply a function to until you have something to apply it to… I hope I’m making sense! Thanks for taking time to reply.

        • Think of it like a tree – you split `a*b*c*d` into (a*b)*(c*d) then you can run a*b and c*d in parallel and then a last * for their results. I think you see how to split this for more elements or more processors/threads 😉

          • Colin A

            ah ha! Yes that is exactly what I meant when I inelegantly said “do you do it like merge sort”. Thanks again Carsten, your blog rocks.

  • Pingback: F# Weekly #10, 2015 | Sergey Tihon's Blog()