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

[Fergus Henderson]

On 23-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> On Thu, 23 Apr 1998, Fergus Henderson wrote:
> 
> > I'm leaning towards `:- assertion' as a better name than `:- pragma assert':
> 
> Agreed, this is much better.  Making it an operator helps, too.

Yes, that's probably a good idea.

> > 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'
> 
> And there should only be one specification per pred or func.

Right.

> > 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.
> 
> I'm not sure there's value in this.  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.
Thus with this proposal, in order to avoid the need for an explicit
spec in those sort of situations, we'd have to allow clauses in a
module's interface section.  But then the interface would be
giving away implementation details: it gives away the fact that the
implementation is the same as the specification.

> How about just:
> 
> 	:- spec associative(F) <=> all [A,B,C] F(A,F(B,C)) = F(F(A,B),C).
> ...
> 	:- assertion associative(+).
> 
> (If this appears in the int module, there should be no need for the module
> qualification.

Presuming that the int module doesn't import any other module
which defines `+', yes.

> Also, I'd expect the usual overloading resolution to handle
> the distinction between associative preds and funcs.) 

That would work OK so long as `associative(pred(...))'
and `associative(func(...))' are defined in different modules
(or different sub-modules).

> This also gives me another idea.  So far we've been talking only about
> properties of the success set of predicates/functions.  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)).

In fact, the current Mercury compiler accepts (but ignores) `where'
conditions on predicates.  There's a type called `condition' defined
in prog_data.m which is used for this.

In NU-Prolog, the requirements here are treated as part of the types of
the arguments (remember Lee's notion of "type").  This works for either
input requirements or output requirements.  However, I can imagine
cases when you might want to specify an output constraint
(i.e. output subtype) on an input mode argument which is stricter
than its input constraint (i.e. its input subtype),
and in that case you really need to attach constraints to the
modes rather than to the types.

 | 	% Types may have arbitrary assertions associated with them
 | 	% (eg. you can define a type which represents sorted lists).
 | 	% Similarly, pred declarations can have assertions attached.
 | 	% The compiler will ignore these assertions - they are intended
 | 	% to be used by other tools, such as the debugger.
 | 
 | :- type condition	
 | 	--->	true
 | 	;	where(term).

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

The Mercury compiler used to accept (and ignore) this syntax too.  I removed
this support when I added support for `type ... where equality is <foo>',
since it caused an obvious conflict.  But we easily could add it back again,
using the syntax `type ... where invariant is ...'.

Perhaps it would be better to use the Mercury syntax for lambda
expressions `pred(X) :- sorted(X)' instead of `X : sorted(X)'.

Note that the current compiler does not actually do anything with such
conditions; it does not even check that they are syntactically correct
or type correct.  Getting it to do that would be a moderate amount
of SMOP.

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