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

[Peter Schachte]

On Thu, 23 Apr 1998, Fergus Henderson wrote:

> > It might be simpler to consider the
> > code for a predicate to be the spec if there isn't a separate spec, rather
> > than vice versa.
> 
> I considered this.  But the trouble with this is that for an exported
> predicate, the spec should usually be part of the module's interface.

Ok, you convinced me.

> > It would also be
> > really useful to be able to specify the input requirements of a predicate or
> > function (other than the types and modes).
> 
> Yes, I agree. 
> 
> NU-Prolog has a syntax for something like this:
> 
> 	:- pred foo(T) where foo(X) : invariant(X).
> 
> 	:- pred merge(list(T), list(T), list(T)) where
> 			(merge(L1, L2, _) : sorted(L1), sorted(L2)).

I think syntactically that's not very good; it would be better to stray from
NU Prolog syntax for this.  I think preconditions are much the same sort of
thing as assertions, and should be syntactically similar.  That's why I
suggested

	:- admissible Atom => Condition.

The idea behind the => is that you are giving a necessary condition for
admissibility of Goal.  If Goal is admissible, then Condition must hold. 
Doing it this way, you can write multiple :- admissible declarations for a
predicate, and they must all be satisfied.  This is good syntactically,
because it allows pattern matching in the "head,"  which is convenient, and
putting all the admissibility conditions in a single term could get messy.
Writing no admissibility conditions for a goal says nothing about its
admissiblity. 

> > Taking this one step further, what I was asking for a few weeks ago was the
> > ability to make assertions about all instances of a given type.
> 
> Yes, NU-Prolog also has a syntax for this:
> 
> 	:- type sorted_list(T) == list(T) where (X : sorted(X)).

Perhaps in the interest of consistency, this should be something like

	:- valid_term T => Conditions.

Again this allows pattern matching, which could be quite useful, eg:

	:- valid_term node(node(_,K1,_), K2, _) => K1 < K2.
	:- valid_term node(_, K1, node(_,K2,_)) => K1 < K2.

Note that these assertions could possibly be used by optimizers in various
ways (using the arrow in the forward direction:  if we assume the term is
valid, we can conclude that the conditions hold), as well as in debugging to
ensure that only valid terms are created.

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.


-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 |