[mercury-users] Mutually exclusive goals

[Robert Bossy]

Hi,

>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.)


Neither do I.


>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.

The point is, the mutual exclusion can't be left unchecked because Mercury
is a LP language (isn't it a good reason?). Hey! What if I declare exclusion
that is not actually correct? My software will
be false (not exclusive) or buggy.



We want to say something like (I didn't use any of the Mercury syntax
intentionally) :


X < Y and X >= Y always fails (can't succeed)
X < Y or X >= Y always succeeds (can't fail)


It seems that we want to declare a determinism according to unification (X
and Y)
instead of mode! My guess is that it would require a major modification of
the language.



>[...]
>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.


That makes a lot to think about! I guess the best way to begin is to gather
examples where mutual exclusion would be useful and meaningful... then
"categorize" them, so we can see what we're dealing with.



Cordialement,
RB

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------