[mercury-users] Re: Question regarding determinism

[Andrew Bromage]

G'day all.

Peter Schachte wrote:

> But I'm still confused.  Why isn't `some [] X' always the same as just `X'? 
> 
> Come to think of it, aren't variables supposed to be quantified in their
> closest enclosing scope?  In this case, the closest enclosing scope for the
> anonymous variable is the list__member goal, so I wouldn't think the
> explicit quantification would be necessary.  Why is it?

Because (currently) for a call to an implied mode, there isn't really a
"scope".  Let me explain...

The problem is that if you have a call to an implied mode:

	:- mode p(in).
	:- mode q(in).

	p(X) :-
		some_goals,
		q(X),
		some_other_goals.

This expands to:

	:- mode p(in).
	:- mode q(in).

	p(X) :-
		some_goals,
		q(V),
		V = X,	% Test unification
		some_other_goals.

The call to q(X) (as opposed to the call to q(V)) doesn't have its own
scope, so V is existentially quantified to the conjunction which contains
it rather than the call.  This is certainly a bug (for reasons detailed
in mercury-users).  One correct way of compiling the above implied mode
is:

	:- mode p(in).
	:- mode q(in).

	p(X) :-
		some_goals,
		some [] (	% Or some [V] if you want it explicit.
			q(V),
			V = X
		),
		some_other_goals.

Now the implied mode call has its own scope, and V is local to it.

The simplest solution is to generate the code above (with existential
quantification), and optimise away the explicit quantification if it
turns out that it makes no semantic difference.  (i.e. Remove a some()
if the inner determinism is the same as the outer determinism.  Is this
the only criterion?  We might even do this already.  Haven't checked.)

Removing unnecessary `some's is good because it gives you more
opportunity for optimisation.  In the above case, if we could remove
the `some', we would have more freedom to move the unification around
if it was more efficient to put it somewhere else.

Cheers,
Andrew Bromage