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

[Fergus Henderson]

On 24-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> On Fri, 24 Apr 1998, Fergus Henderson wrote:
> 
> > So why not just use `assertion'?
> > 	:- typeclass foo(T) where [
> > 		pred '>='(T, int),
> > 		mode '>='(in, in) is semidet,
> > 		assertion X >= 0
> > 	].
> 
> [long explaination for why this means the right thing snipped]
> 
> How about this, instead:
> 
> 	:- typeclass number(T) where [
> 		pred '>='(T, T),
> 		func zero = T,
> 		mode '>='(in, in) is semidet,
> 		valid_term X:T => X >= zero
> 	].
>
> I find this clearer.

Well, if we go with the `valid_term' syntax, that would be fine.
Of course the type qualifier `:T' could be inferred, so we could
make such type qualifiers optional, although probably in this case
the code is clearer with the explicit type qualifier.

> > I suppose if we have support for run-time checking of certain specialized
> > kinds of assertions, such as preconditions, postconditions, and invariants,
> > then we will need some special syntax for them to distinguish them from
> > general assertions.
> 
> The set of declarations I proposed does this.  `valid_term' and `admissible'
> describe things that would be interesting to check at runtime or possibly to
> check at compile time, while `assert' and `specification' give claims about
> the implementation.  Maybe the difference between the two is in culpability: 
> if a `valid_term' or `admissible' statement is violated, the caller did
> something wrong.  If an `assertion' or `specification' is violated, then the
> predicate itself is buggy.  Well of course in any of these cases the
> declarative information itself could also be wrong.

In the general case of an assertion, there may be many predicates and functions
involved, so you may not be able to pin down the responsibility so easily
(e.g. consider `:- assertion a + b + c > 30.').
In the case of a specification being violated, either the predicate or the 
specification is wrong, but the failure may be due to a bug in some
code called by the predicate or the specification, rather than in
the code for the predicate or specification themselves.

I think it is important to distinguish between specifications,
which in general will often *not* be executable (if most of your
specifications are executable, then it's a sign that you are not
writing your specifications at a high enough level),
and postconditions that could reasonably be checked at runtime.

> > Since we can have multiparameter type classes, the invariant
> > for an type class of arity N would have to be a predicate of arity N.
> 
> Yuck.
...
> This one has me baffled.

Yes, I was confused -- ignore that one.
You should have separate invariants for each type in a type class.
If we want to use the `where invariant is' syntax, then for type
classes it should probably look like this:

 	:- typeclass tc(T1, T2, T3) where [
 		invariant(T1) is p1,
 		invariant(T2) is p2,
 		invariant(T3) is p3,
		...
	].

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