[m-dev.] Re: assertions (was: Assocative predicates)

[David Glen JEFFERY]

On 24-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> On Fri, 24 Apr 1998, David Glen JEFFERY wrote:
> 
> > > Perhaps the valid_term syntax will need to be
> > > broadened to make it possible to refer to instances of the type parameters
> > > of the instances of the class.
> > 
> > I think you can get the same effect by making assertions about type class
> > methods and having the compiler (or theorem prover, or whatever) check that
> > assertion about that method for each instance declaration.
> 
> Right, but you still can't specify invariants about the types themselves. 
> I can't think of any good examples at the moment; here's the best I can
> think of.  You might have a non_negative_number type class, with all the
> usual operations, each with all the usual assertions.  But you'd still want
> to assert that every element of every type in the class is >= 0.

Ah yes, I think you're right. (Although to make your example more plausible,
the invariant would be that for every value, >= zero holds, where zero is
a function of the type class).


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
MEngSc student,                 |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.