[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, David Glen JEFFERY wrote:
> 
> > > Perhaps the valid_term syntax will need to be
> > > broadened to make it possible to refer to instances of the type parameters
> > > of the instances of the class.
> > 
> > I think you can get the same effect by making assertions about type class
> > methods and having the compiler (or theorem prover, or whatever) check that
> > assertion about that method for each instance declaration.
> 
> Right, but you still can't specify invariants about the types themselves. 
> I can't think of any good examples at the moment; here's the best I can
> think of.  You might have a non_negative_number type class, with all the
> usual operations, each with all the usual assertions.  But you'd still want
> to assert that every element of every type in the class is >= 0.

So why not just use `assertion'?

	:- typeclass foo(T) where [
		pred '>='(T, int),
		mode '>='(in, in) is semidet,
		assertion X >= 0
	].

Note that implicit universal quantification means that the assertion
is the same as

		assertion all [X] X >= 0

and since X has type `T' here (this is inferred from the type of `>=')
that really means

		assertion all [X in T] X >= 0

So the declarative semantics of this assertion is what you want.
The question then is about the operational semantics.

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.  For example, the compiler would only do type checking
for general assertions, but for assertions which will actually be checked
at runtime, it needs to do mode checking too.
If we have preconditions (checked on entry),
postconditions (checked on success), and invariants for
concrete types (checked when you construct a value of that
type), then it would also make sense to have invariants for
abstract data types (checked when converting a value of a concrete
type to a type-class-constrained type).

If the syntax for an invariant on a concrete class is

	:- type <typedefn> where invariant is <predname or lambda-expr>.

then the natural thing to do for type class invariants would be
to use the same kind of syntax:

	:- typeclass <class> where [
		invariant is <predname or lamda-expr>,
		pred(...) is ...
	].

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.

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 :- ...),
		...
	].
	:- pred p1(T).

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