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

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