[mercury-users] Constraints and conditionals in Mercury

[Ralph Becket]

Richard A. O'Keefe, Friday, 11 April 2008:
> It has been just been pointed out to me that there is a major bug in
> SWI Prolog caused by the interaction of cuts and constraints.
> Basically, in (p -> q ; r), if p has created some constraints which
> remain suspended, it may appear to have succeeded, with the conditional
> committing to q, even though the suspended constraints are not
> satisfiable.
> 
> Mercury has conditionals and constraints.   I cannot believe that the
> Mercury team would find such a state of affairs tolerable, as I do not.
> What does Mercury actually _do_ to make this work?

Mercury solves this problem for "ground" types by requiring that p not
bind any variables non-local to the if-then-else.

For "solver" types, whose variables can be constrained without becoming
ground, we need to be more careful.  Non-ground solver type variables
typically have a special inst, 'any'.  Currently any if-then-else goal
with a solver variable (with inst 'any') in the condition is considered
impure and must be labelled as such.  It is the programmer's
responsibility to promise away the impurity if that is warranted.

For example, if X and Y are solver variables then

	promise_pure ( if list.length([X, Y]) > N then q else r )

[the promise is sound because list.length will not constrain X or Y]

	promise_impure ( if X > Y then q else r )

[the promise is required to acknowledge to the compiler that the
condition does not respect the declarative semantics.]

Omitting either promise is an error.

We recognise that this is not an attractive solution and we have a
proposal to add 'constraint' as a new kind of 'pred' to the language.
The difference being that a constraint may bind any solver variable
reachable from its arguments whereas a pred may not (there are some
subtleties to do with higher order preds taking constraint arguments,
but you get the idea).  The purity rule would then only be required for
constraints appearing in condition goals.

-- Ralph
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------