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

[Peter Schachte]

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.

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

> If the syntax for an invariant on a concrete class is

I still prefer the `:- valid_term' syntax, but if you're intent on the
`where' syntax, how about using `each' instead of `invariant'? 

	:- type sorted_list == list where each is sorted.

just reads a lot better than

	:- type sorted_list == list where invariant is sorted.

or

	:- type sorted_list == list where invariant is
		(pred(X) :- sorted(X)).

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

> Alternatively, we could explicitly name which types the invariant
> applies to:
> 
> 	:- typeclass tc(T1, T2, T3) where [
> 		invariant(T1) is p1,
> 		invariant(T2, T3) is (pred(T2::in, T3::in) is semidet :- ...),

This one has me baffled.  I assume you're trying to say that for every X in
type T2 and for every Y in T3, some property holds.  I can't think of a case
where you'd want to say that.  But anyway, which T2 here refers to a type
and which to an instance?  How do you say something about all pairs (X, Y)
where both X and Y are of type T2?

> 	].
> 	:- pred p1(T).


-Peter Schachte               | This sentence contradicts itself - no
mailto:pets at cs.mu.OZ.AU       | actually it doesn't.
http://www.cs.mu.oz.au/~pets/ |     -- Hofstadter 
PGP: finger pets at 128.250.37.3 |