[m-dev.] Mutual Exclusivity & Exhaustiveness

[Peter Schachte]

On Fri, Jan 04, 2002 at 03:02:11PM +1100, Fergus Henderson wrote:
> On 04-Jan-2002, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> > On Thu, Jan 03, 2002 at 09:16:14PM +1100, Simon Taylor wrote:
> > > Would something like the following be better?
> > > 
> > > :- promise_determinism
> > > 	all [X, Y]
> > > 		( foo(X, Y)
> > > 		; bar(X, Y)
> > > 		)
> > > 		is multi.
> > 
> > I understand and appreciate the meaning behind this syntax.  In some ways
> > it's very nice and logical.  As you say, it matches how it will be used.
> > It's just that I don't think it reflects the way people will naturally tend
> > to think about what they're saying about the relationship between these
> > predicates, and therefore I see it as more error-prone than the more direct
> > statement about mutual exclusivity or exhaustiveness.  And since these are
> > unchecked promises, being more error-prone is a serious problem.
> 
> I don't think mutual exclusion is necessarily the right concept to
> use here anyway.  The property that we need for determinism analysis
> is that the disjunction has at most one distinct solution; mutual
> exclusion of the disjuncts is a sufficient but not necessary condition.
> 
> For example, if you have
> 
> 	foo(yes, 1).
> 
> 	bar(yes, 1).
> 	bar(no, 2).
> 
> 	:- pred p(X::in, Y::out) is det.
> 	p(X, Y) :- foo(X, Y) ; bar(X, Y).
> 
> then for any given X the disjunction `foo(X, Y) ; bar(X, Y)' has
> at most one solution Y, even though the disjuncts are not mutually
> exclusive (for X = yes, both disjuncts will succeed, but they'll
> return the same answer Y = 1).  So it would be nice if the compiler were
> to allow code which relies on this, such as p/2 here.

I don't think this proposal is a good idea because it's hard to understand.

Again, since this is an unchecked assertion, I think it's important that the
assertion be crystal clear and simple, and I don't think Fergus' suggestion
is.  At least not for users.  When they're frustrated that the compiler won't
accept their code as deterministic, they'll try putting in more or less
random :- promise_at_most_one_solution declarations until the compiler
accepts it.  But if the declaration is as simple as claiming that two goals
are mutually exlusive, users are less likely to take wild guesses (because
they'll understand what the guesses mean).  So although
exclusivity/exhaustiveness declarations are strictly less powerful than
Fergus' suggestion or Simon's original suggestion, I think they're preferable
because they're powerful enough for most uses, and easier to understand.


BTW, I think Fergus's example could be better handled by a simpler assertion:

	:- promise foo(X,Y) => bar(X,Y).

This makes it clear that the clause can be rewritten

	p(X, Y) :- bar(X, Y).

which will of course be det in the same modes as bar/2.  It also tells us
that

	q(X, Y) :- foo(X,Y), bar(X, Y).

can be rewritten

	q(X, Y) :- foo(X, Y).

which the promise_at_most_one_solution version doesn't.


> These both solve the code duplication problem for things
> that are both exhaustive and exclusive.

The code duplication problem is not a problem.  You just allow both
declarations to be given together:

	:- promise_exclusive promise_exhaustive 
		X < Y,
		X = Y,
		X > Y.

One other thing:  these declarations should be allowed in type class
declarations so that exclusivity and exhaustiveness to be required of class
members.

-- 
Peter Schachte              I have not yet begun to procrastinate. 
schachte at cs.mu.OZ.AU        
www.cs.mu.oz.au/~schachte/  
Phone: +61 3 8344 9166      
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------