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

Reply via email to