Monoids exploiting static constraints

Monoids.fs

namespace Monoids

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