Create a gist now

Instantly share code, notes, and snippets.

Monoids exploiting static constraints
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment