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

[David Glen JEFFERY]

> > This also gives me another idea.  So far we've been talking only about
> > properties of the success set of predicates/functions.  It would also be
> > really useful to be able to specify the input requirements of a predicate or
> > function (other than the types and modes).
> 
> Yes, I agree. 
> 
> NU-Prolog has a syntax for something like this:
> 
> 	:- pred foo(T) where foo(X) : invariant(X).
> 
> 	:- pred merge(list(T), list(T), list(T)) where
> 			(merge(L1, L2, _) : sorted(L1), sorted(L2)).
> 
> In fact, the current Mercury compiler accepts (but ignores) `where'
> conditions on predicates.  There's a type called `condition' defined
> in prog_data.m which is used for this.
> 
> In NU-Prolog, the requirements here are treated as part of the types of
> the arguments (remember Lee's notion of "type").  This works for either
> input requirements or output requirements.  However, I can imagine
> cases when you might want to specify an output constraint
> (i.e. output subtype) on an input mode argument which is stricter
> than its input constraint (i.e. its input subtype),
> and in that case you really need to attach constraints to the
> modes rather than to the types.

Is this really true? Maybe I haven't had enough coffee today (hmmm, good
idea...) but I don't see how you can have an output constraint that is 
different to an input constraint. Surely the set of terms that is true in the
success set in one mode should be the same in any other mode. Am I missing
your point?


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
MEngSc student,                 |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.