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

[Peter Schachte]

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.


-Peter Schachte               | This sentence contradicts itself - no
mailto:pets at cs.mu.OZ.AU       | actually it doesn't.
http://www.cs.mu.oz.au/~pets/ |     -- Hofstadter 
PGP: finger pets at 128.250.37.3 |