more on Monoids in F# – exploiting static constraints

Just a quick follow up on yesterdays post on Monoids.

Maybe you did not like the way the structure of the monoids was passed around using a simple record and indeed there is a way to define the Z and ++ as generic operators by exploiting Statically Resolved Type Parameters in F#.

As far as I know this was first mentioned here and there is a great project on github using this FsControl.

Rewriting some of the instances this way can look something like this:

open FsCheck
open FsCheck.Xunit

type Neutral() =
    static member val Instance = Neutral()
        
    static member Neutral (_:list<_>, _:Neutral) = []
    static member Neutral (_:'a->'a,  _:Neutral) = id

    static member inline Invoke() = 
        let inline neut  (a:^a, b:^b) = 
            ((^a or ^b):(static member Neutral:_*_->_) 
             b, a)
        let inline neut' (a:'a) = 
            neut (a, Unchecked.defaultof<'b>) :'b
        neut' Neutral.Instance

type Operator() =
    static member val Instance = Operator()
        
    static member Op (a:list<_>, b:list<_>) = a @ b
    static member Op (f:'a->'a,  g:'a->'a)  = f >> g

    static member inline Invoke (a:'a) (b:'a) : 'a = 
        let inline op (_:^M, x:^v, y:^v) = 
            ((^M or ^v) : (static member Op:_*_->_) x, y)
        op (Operator.Instance, a, b)

[<AutoOpen>]
module Operators =
    let inline Z ()     = Neutral.Invoke ()
    let inline (++) x y = Operator.Invoke x y

type NonNullString = 
    NNS of string with
    static member Neutral (_,_)          = NNS ""
    static member Op      (NNS a, NNS b) = NNS (a+b)

type Prod =
    Prod of int with
    static member Neutral (_,_)            = Prod 1
    static member Op      (Prod a, Prod b) = Prod (a*b)

type Generators() =
    static member NonNullString : Arbitrary<NonNullString> =
        let nns s = 
            if System.String.IsNullOrEmpty s 
            then "" 
            else s
            |> NNS
        { new Arbitrary<NonNullString>() with
            member __.Generator = 
                Arb.generate |> Gen.map nns 
        }


module ``check Monoid axioms for int-Lists`` =
    type T = list<int>

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

    [<Property>]
    let ``concatenation is commutative``(a : T, b : T, c : T) =
        a ++ (b ++ c) = (a ++ b) ++ c


[<Xunit.ArbitraryAttribute(typeof<Generators>)>]
module ``check Monoid axioms for NonNullString`` =
    type T = NonNullString

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

    [<Property>]
    let ``concatenation is commutative``
        (a : T, b : T, c : T) =
            a ++ (b ++ c) = (a ++ b) ++ c

module ``check Monoid axioms for Prod`` =
    type T = Prod

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

    [<Property>]
    let ``multiplication is commutative``
        (a : T, b : T, c : T) =
            a ++ (b ++ c) = (a ++ b) ++ c

You can find a gist containing the relevant code here.

my take on it

First let me make clear that I love how those guys managed to put this all together! – this is a major hack of F# and it’s type-system. It’s one of the most clever thing I saw using F# and I am really impressed by all Gustavo did there.

But for me this is just to much boiler-plate only to get simulated type-class support that really should be there in the language itself (or maybe better: a ML-like module system). In the end at this point this is just used to get function-overloads based on type (a great feature). At the moment I prefer to use modules (like List.map, Option.map) – yes the compiler could know this but for me it’s no big deal.

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

Spartakiade

2015, Berlin / März

Spartakiade

Spartakiade 20015

Die Community-Konferenz Spartakiade vom 21.–22. März 2015 in Berlin bietet Workshops zum Mitmachen an. Bei der Spartakiade kennt man keinen Zeitdruck und lässt Teilnehmer sich ausführlich und intensiv mit einem Thema beschäftigen. Die Dauer der Workshops geht weit über die Vortragsdauer der üblichen 60–90 Minuten auf „klassischen“ Konferenzen hinaus, die meisten Workshops sind ganztägig. Und weil das wie beim Sport herausfordernd werden kann, heißt die Konferenz „Spartakiade“ – namentlich auch bekannt als Sportveranstaltung.

Workshops sind für jeden Schwierigkeitsgrad aus der Softwareentwicklung dabei – etwas für Leichtathleten, Kraftsportler oder Mehrkämpfer und die ganze Mannschaft. Inhaltlich geht es um Agile Games, Event Storming, Git, Node.js / AngularJS, Raspberry Pie, Funktionale Programmierung, Microsoft Lync und vieles mehr.

Ich selbst bin (wie hier schon beschrieben) mit meinem Workshop zu Funktionale Programmierung mit dabei.

Umfrage

Ihr könnt in der nächsten Zeit noch mitbestimmen, welche Sprache ich euch reindrücken soll:

bitte in folgender Programmiersprache

View Results

Loading ... Loading ...

Momentan sieht es nach F# aus!

(Schöner wäre ein kleiner Kommentar oder ein Nachricht – damit ist es für mich leichter Teilnehmer von Seitenbesuchern zu unterscheiden)

Anmeldung

Die Anmeldung ist ab sofort möglich unter: spartakiade.org

Ich freu mich auf Euch!