assertions (was: Assocative predicates)

[Fergus Henderson]

I'm leaning towards `:- assertion' as a better name than `:- pragma assert':

	*  `assertion' is better than `assert' because
	   we want to use declarative nouns rather than imperative verbs --
	   using the imperative verb suggests side effects, and would not
	   doubt cause some confusion with Prolog's `assert';

	*  assertions are important enough that they should be a part of
	   the language proper, not pragmas.

I think we should also allow `:- specification' (or perhaps `:- spec')
with the same semantics as `:- assertion' but with an additional
restriction that the assertion must be of the form `p(Vars) <=> Goal'
or `f(Vars) = Expression <=> Goal' with the `<=> Goal' part optional,
where Vars are distinct variables.  That is, a specification is an
assertion that completely specificies the semantics for a particular
predicate or function.

Often the code for a procedure is identical to its specification,
so probably it would make sense to use the specification as the default
implementation if there are no clauses for the procedure.

On 23-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> ... I still think there is something to be said for using words people
> recognize like "associative," "commutative," etc.  I suppose that can be
> done in comments, but how about allowing users (and the standard library) to
> define properties.  Maybe something like
> 
> :- pragma assertion(associative_function(F) = (F(A,F(B,C)) = F(F(A,B),C))).
> :- pragma assertion(associative_predicate(P) = (
> 	P(A,B,C), P(C,D,E) <=> P(B,C,F), P(A,F,E)
> ).

That's a good idea.  However, these "properties" are in many ways similar
to ordinary predicates, so I'd prefer a syntax that more closely reflected
this.  Indeed, this could almost be done just using ordinary predicates,
without introducing any new construct at all:

	:- pred associative_function(func(T1, T2) = T3).
	:- specification(associative_function(F) <=>
			all [A, B, C] (F(A,F(B,C)) = F(F(A,B),C))).

	...
	:- assertion(associative_function(int:'+'))).

The only problem with this is that the compiler will complain about
there being no modes for `associative_function'.
One way of working around this would be to use a "not_reached" mode

	% na stands for "not applicable"
	:- mode na == not_reached -> not_reached.

	:- mode associative_function(na) is erroneous.

However, it might be better to have some special syntax for this
(any suggestions?).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.