On 10/13/05, Dave Whipp <[EMAIL PROTECTED]> wrote: > (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:
I've been thinking about this. If we have a type inferencer, we know that any function we define to be N,N->N will be that way. The only items we have to show is for all a in N, there is a unique succesor which is also in N and that for all b in N, b != 1, there is a unique predecessor. If we have that, then we get the laws of arithmetic. Is it possible to put that into the type inferencer if the types are defined as iterators? Kind of like Church numbers, but in P6 notation. I think that by defining our types as iterators, we can satisfy the succ/pred requirements of Peano's, meaning we have the arithmetic rules. Rob
