[mercury-users] Newbie problem. :)

[Richard A. O'Keefe]

I wrote:
	> Why should I be forbidden to say that
	>     :- positive_definite(M), singular(M).
	> just because I didn't write *all* the predicates in the rule?
	
Peter Schachte replied:

	The problem is that if you do, and if someone later edits the linear
	algebra pacakge, they don't know that their predicate has to be
	mutually exclusive with someone else's.

It doesn't matter.
Not at all.

Remember, exclusion is about MEANING, not implementation.
If someone edits the linear algebra package, they can do
what they please as long as they don't change the MEANING
of the exported predicates.  If they do change the meaning
of an exported predicate like singular/1, without renaming
it, then you are stuffed ANYWAY.

How can a system keep track of a dependency like this?
The same way it would keep track of any other use:  using
an imported predicate in a negative rule makes *exactly*
the same reference to its interface and meaning that any
*other* reference to that predicate would.

	The only sensible way I can see to allow the declaration of
	mutual exclusion among predicates in multiple modules is for that
	declaration to be repeated in the interface of each module that
	defines a predicate involved in that exclusion.  At least then
	the declaration can be seen as part of the interface for that
	predicate.

But it *isn't* part of the interface for that predicate.
I was going to say "that's ridiculous", but to be fair, I suppose
it isn't *obviously* ridiculous.  If I write a

    :- pred perfect_number(integer).
    :- mode perfect_number(in) is semi_det.

(and possibly other modes), then the negative rule

    :- perfect_number(N), N < 6.

is *TRUE*, but it is *NOT* in any reasonable sense part of the
interface of "<".

There seems to be some sort of magical belief that it is illegal,
immoral, or fattening to mention any property of an imported predicate
which the compiler cannot verify.  But this belief is suddenly ignored
when it's a question of a property that is used in a direct *call*.
Apparently it is ok for me to write

    (  singular(X) -> ...
    ;  positive_definite(X) -> ...
    ...
    )

which will *BREAK* if someone edits the linear algebra package so that
some positive definite matrices come to be reported as singular, but
it's NOT ok for me to be up front and say that I *rely* on these
predicates being exclusive and then leave it to the compiler to
exploit the fact.  This baffles me, because the *only* maintenance
difference between

    (  singular(X) -> ...
    ;  positive_definite(X) -> ...
    )

and

    :- singular(X), positive_definite(X).
    ...
    (   singular(X), ...
    ;   positive_definite(X), ...
    )

is that in the version with the negative rule, the crucial information
is written *SOMEWHERE*, while in the present state of affairs it is
written *NOWHERE*.  

Note that the compiler can be asked to debug the use of negative rules.
Suppose we have

    :- p(X), q(X), r(X).
    ...
    (   p(X), r(X), ...
    ;   q(X), ...
    )

The "fast" version I have already described.  It is

    (   p(X), r(X) -> ...
    ;   q(X), ...
    )

But a "debugging" version

    (   p(X), r(X) ->
	( q(X) -> REPORT NEGATIVE RULE ERROR; true), ...
    ;   q(X), ...
    )

is also possible.

In fact, I honestly don't see why negative rules couldn't legitimately
be stated *anywhere*; if a module depends on p(X) and q(X) being
exclusive, it doesn't matter *where* p(X) and q(X) come from, the
dependency *exists*, and it is better to say it than not say it,
and it is better to be able to automatically check it at run time
than not to be able to check it automatically at all.

It is best of all if properties can be automatically verified at
compile time.  It is certainly reasonable to demand that a module
not *export* a negative rule unless the rule mentions at least one
of the exported predicates of the module.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------