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

[David Glen JEFFERY]

On 24-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> 
> So in summary, here are the new declarations/directives I'd like:
> 
> 	:- specification Atom <=> Body.
> 	:- assertion Body.
> 	:- admissible Atom => Body.
> 	:- valid_term Term => Body.	% or maybe Term::Type => Body.
> 
> The only other thing I can think of is that these should be allowed in type
> classes, too, to add extra constraints to, and information about, the
> instances of the class.  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.


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.