[mercury-users] Request for comments on this code

[Mark Brown]

On 10-Jul-2006, Ian MacLarty <maclarty at csse.unimelb.edu.au> wrote:
> On Sun, Jul 09, 2006 at 05:13:41PM +1000, Mark Brown wrote:
> > Having said that, I think we should re-open the case for `&&'.  It would
> > be particularly useful for applications that do constraint solving using
> > solver types.  For example, a typical application would do the following:
> > 
> > 	post_constraints_1(...),
> > 	post_constraints_2(...),
> > 	...,
> > 	label_vars(...)
> > 
> > The labelling step is declaratively a NOP (and is perfectly pure), but you
> > always want it to be done after the constraints have been posted.  Moreover,
> > it is nondet so you can't thread the IO state through.  Currently, the
> > only options are to use impurity or to use the strict sequential semantics,
> > both of which have drawbacks.
> > 
> 
> You say these are the only options.  What about threading some other
> state that needn't be di, uo?  Wouldn't that also be an option?

Well, yes, that is a third option.  But by "constraint solving using solver
types" I meant using an interface that doesn't require any state to be
threaded through.

In any case, threading a state through has much the same drawbacks as
using the strict sequential semantics.  Namely, when reasoning about
the operational semantics you will need to consider the ordering of all
the conjuncts, when really the only requirement is to consider whether
the labelling step comes last.  The order in which constraints are posted
is generally not important.

For example, the goals

	foo(...),
	bar(...)
	&&
	label_vars(...)

and
	bar(...),
	foo(...)
	&&
	label_vars(...)

are obviously equivalent declaratively, and the placement of `&&' is an
indication from the author that operationally they are close enough.  But
for the goals

	foo(..., !S),
	bar(..., !S),
	label_vars(..., !S)

and
	bar(..., !S),
	foo(..., !S),
	label_vars(..., !S)

neither of these points is directly apparent.  You would need to reason
about the semantics (declarative and operational) of the three predicates
to draw the same conclusions.  In particular, you would need to know that
"bar" is not in fact an "ask" constraint, the effect of which will depend
on the current state.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at csse.unimelb.edu.au
administrative address: owner-mercury-users at csse.unimelb.edu.au
unsubscribe: Address: mercury-users-request at csse.unimelb.edu.au Message: unsubscribe
subscribe:   Address: mercury-users-request at csse.unimelb.edu.au Message: subscribe
--------------------------------------------------------------------------