(ref: http://svn.openfoundry.org/pugs/docs/notes/theory.pod)
> theory Ring{::R} {
> multi infix:<+> (R, R --> R) {...}
> multi prefix:<-> (R --> R) {...}
> multi infix:<-> (R $x, R $y --> R) { $x + (-$y) }
> multi infix:<*> (R, R --> R) {...}
> # only technically required to handle 0 and 1
> multi coerce:<as> (Int --> R) {...}
> }
>
> This says that in order for a type R to be a ring, it must
> supply these operations. The operations are necessary but
> not sufficient to be a ring; you also have to obey some
> algebraic laws (which are, in general, unverifiable
> programmatically), for instance, associativity over
> addition: C<(a + b) + c == a + (b + c)>.
I started thinking about the "in general, unverifiable programmatically"
bit. While obviously true, perhaps we can get closer than just leaving
them as comments. It should be possible to associate a
unit-test-generator with the theory, so I can say:
theory Ring(::R) {
...
axiom associative(R ($a, $b, $b)) {
is_true( ((a+b)+c) - (a+(b+c)) eqv R(0) );
}
...
}
And then say "for type T, please generate 1000 random tests of T using
axioms of Ring".
In an ultra-slow debug mode, the aximons could be propagated as post
conditions on every public mutator of T, so that we test them
continuously in a running application (or tes suite).
