[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 considered this.  But the trouble with this is that for an exported
> > predicate, the spec should usually be part of the module's interface.
> 
> That's not clear to me.  This raises the issue DJ mentioned in a more recent
> message:  are the assertions and preconditions part of the declaration of
> the predicate, or part of the definition?

Asking whether they're part of the declaration or part of the
definition is the wrong question, IMHO.  You should be asking about
whether they're part of the interface or the implementation.

Preconditions must be part of the interface, since the caller needs
to know the preconditions before calling.
Any other assertions (including specs) may be part of the interface,
but equally they might not be -- it depends on how much information
you, the designer of this module, want to make visible to the users of
this module.  The language should allow either.

> are the assertions and preconditions part of the declaration of
> the predicate, or part of the definition?
> If the latter, then I don't see a
> problem.  I briefly considered the former, which could be very nice, but
> decided it would be a lot to require of implementors.  For example, it'd be
> nice to put this into the int and float modules:
> 
> 	:- assertion X < Y <=> \+ X >= Y.
> 	:- assertion X =< Y <=> ( X < Y ; X = Y ).
> 	:- assertion X < Y <=> Y > X.
> 	...

Yes, definitely.

> and have determinism analysis figure out that
> 
> 	min(X, Y) = X :- X =< Y.
> 	min(X, Y) = Y :- X >= Y.
> 
> is actually deterministic in the forward mode.

That would seem nice, but it would be a lot to require of implementors.
I don't think we should consider it at the current point in time.

> My point is that if you're just going to use assertions for (maybe) checking
> the validity of a predicate definition, and for various optimizations, then
> I don't see why it should to be part of the interface.  Optimizations are
> allowed to break encapsulation.

A very important reason for making assertions part of the language
is so that *programmers* can use them, e.g. for documenting interfaces.
If we're trying to do programming by contract, then assertions
may be a big part of the contract.

> > In NU-Prolog, the requirements here are treated as part of the types of
> > the arguments (remember Lee's notion of "type").
> 
> I had in mind something more powerful than this.  I want to be able to make
> statements about relationships among arguments.

I guess I wasn't clear -- NU-Prolog does support that.

	:- pred p(T1, T2) where (p(X, Y) : some_relation(X, Y)).

> > > 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)).
> 
> What's X?  It looks kind of like a lambda variable.

Right.

> Maybe something like
> 
> 	:- type sorted_list(T) == list(T) where sorted.
> 
> would be clearer (the where part always being a closure expecting one
> argument).

Yep, that's basically what I meant when I suggested
using the Mercury lambda syntax rather than this NU-Prolog `Var : Goal'
syntax.

The only thing is that `... where invariant is sorted.'
reads a little wierdly -- that's why I wrote
`where invariant is (pred(X) :- sorted(X))'.

> I assume I could also put a where clause on a discriminated
> union type?

Yep.

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