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

[Peter Schachte]

On Thu, 23 Apr 1998, Fergus Henderson wrote:

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

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

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.  Note that I made it extra
tricky by making min(X, X) have two identical solutions.  The point being
that this would be very nice, and I'd really like to see it, but it does
seem like a lot to ask a compiler writer to handle.

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.

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

> > 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.  Maybe something like

	:- type sorted_list(T) == list(T) where sorted.

would be clearer (the where part always being a closure expecting one
argument).  I assume I could also put a where clause on a discriminated
union type?  For lots of types the unconstrained type isn't useful (eg a
map:  there are no unsorted maps).


-Peter Schachte               | The secret of being miserable is to have the
mailto:pets at cs.mu.OZ.AU       | leisure to bother about whether you are
http://www.cs.mu.oz.au/~pets/ | happy or not. The cure is occupation.
PGP: finger pets at 128.250.37.3 |     -- George Bernard Shaw