[mercury-users] Mutually exclusive goals

[Peter Schachte]

On Wed, Jul 07, 1999 at 04:33:07PM +0200, Robert Bossy wrote:
> Finally Rob suggested that A < B and A >= B would be mutually
> exclusive for integers. In that case, the mutual exclusion isn't
> something we say but something we prove... it is a consequence of the
> fact that integers are ordered. 

Actually, I think it's more than that:  it's part of the definition of
being ordered, or maybe part of the definition of <, =, and >.  But
whichever way you look at it, there are two choices:

    1.  build into Mercury an understanding of what ordered means; or
    2.  build into Mercury the ability to declare mutual exclusion.

(Actually, of course, there's the third:

    3.  don't allow mutual exclusion other than implied by
        discriminated union types to influence determinacy analysis.

But I don't like that choice, for reasons I outlined earlier.)

However, as you say, there are plenty of other cases where you'd like
to be able to assert mutual exclusion, and in which it wouldn't make
much sense for Mercury to build in knowledge of exclusion.  Therefore,
even if you take option 1, you really need to take option 2 anyway.
So we might as well just take option 2, and not 1.


> My suggestion is to define a typeclass where there are two
> predicates equality('=') and order('<').


I think it's a very good idea to create an `ordered' type class, and
probably `partial_order' and `total_order' subclasses, as well.  <, =,
and > are exclusive for all of them, but only exhaustive for total
orders.  The `ordered' class should make use of option 2 to declare
the exclusiveness of <, =, and >, and `total_order' should also
declare their exhaustiveness.  Further, `ordered' should declare that

	:- assert A < B ; A = B <=> A =< B.
	:- assert A > B ; A = B <=> A >= B.

These statements should all be part of the interface of this type
class, since every instance should satisfy these constraints.

Ideally, the programmer would then be allowed, but not required, to
define =< and >=.  If they aren't defined, the compiler should be able
to use these assertions to generate definitions from <, =, and >.  In
fact, since = is defined by default, for a total order, the compiler
should be able to generate definitions for all 6 predicates from = and
any one of <, =<, >=, or > (using negation).  For some types it's more
convenient to define < as the primitive operation, while for others =<
is easier.


> Now, not all mutually exclusive goals are a consequence of
> order. But we should think about what makes them live before
> directly declaring them.


Agreed.  To me, the question is: is mutual exclusion an artifact of
the implementation, or inherent in the specification?  In the latter
case, it should be part of the interface, in the former, it should
just be part of the implementation.  For inherent exclusion, there's a
a separate question: is this a property of a class of types, or is it
just true of this one type?  In the former case, the exclusivity
assertion belongs in a type class.

-- 
Peter Schachte                     You can tell the ideals of a nation by
mailto:schachte at cs.mu.OZ.AU        its advertisements.
http://www.cs.mu.oz.au/~schachte/      -- Norman Douglas 
PGP: finger schachte at 128.250.37.3  
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------