[m-dev.] Re: assertions (was: Assocative predicates)
pets at students.cs.mu.OZ.AU
Fri Apr 24 16:35:39 AEST 1998
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.
:- 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.
> 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 220.127.116.11 |
More information about the developers