I was looking at Wikipedia’s article regarding Monoids, and decided that it was interesting to make a post regarding the section “Monoids in Computer Science” http://en.wikipedia.org/wiki/Monoid#Monoids_in_computer_science.
So there they have posted this formula:
And let’s also take a look at Haskell’s definition for fold:
(>>>) = (++)
fold [] = []
fold (m:l') = m >>> (fold l')
Notice the relation between the formulas? Just replace >>> with *, and there you have it!
Regarding the types, in Haskell we have:
*Main> :t fold
fold :: [[a]] -> [a]
And in Mathematics, we have:
fold: M* -> M
The star here represents Kleene’s star, and it is defined to be all concatenations on the elements of the set M, including the empty string (). Example, if M = {a, b} then M* = {(), (a), (b), (a,a), (a,b), (b,b), (b,a), (a,b,a), …}. So what this means is, that if we have M defined as list of integers, then M* would be list of list of integers (which is the result of list concatenation of the elements of M).
And what is fold? Well, fold basically takes a Monoid and applies its operation. Now that we have these two formulas, we can show how fold operates on a Monoid.
Let’s consider the Monoid M ([Int], ++, []). First, to prove that this triple makes a monoid, we must first take a look at the definition of ++:
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys) (*)
1. Closure
Namely, the (++) is the list concatenation operator, and when we concatenate two lists, we get list as an output, according to ++ definition.
2. Associativity
(xs ++ ys) ++ zs = xs ++ (ys ++ zs), order of evaluation will not change the resulting list
To prove this, we again need to look at ++ definition.
We can use Structural Induction in order to prove associativity.
Base case: If we let x = ys + zs, then [] ++ x = x by definition, LHS equals to x. and for the RHS, we get “” + ys = ys by definition, so ys ++ zs == x, and so LHS = RHS.
Inductive step: Assume that (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
We need to prove that ((x:xs) ++ ys) ++ zs = (x:xs) ++ (ys ++ zs)
LHS: by (*) = (x : (xs ++ ys)) ++ zs => let xs ++ ys = p => x : p ++ zs = x : ((xs ++ ys) ++ zs)
RHS: by (*) = x : (xs ++ (ys ++ zs)) => by assumption => x : ((xs ++ ys) ++ zs)
So we get that LHS = RHS.
3. Identity
The empty list [] is the identity here, because [] ++ ys or ys ++ [] always equals to ys, according to ++ definition (already proved by base case in 2).
Now, we can start playing around with our fold:
*Main> fold [[1,2], [3]] -- per Monoid M
[1,2,3]
*Main> fold [['a'],['b'],['c']] -- same as Monoid M, but operates on set [Char] instead of [Int]
"abc"
bor0's reflective blog 