[m-dev.] Re: bug in scoping for higher order terms

[Peter Schachte]

On Sat, Mar 06, 1999 at 03:06:10AM +1100, Fergus Henderson wrote:
> On 04-Mar-1999, Juergen Stuber <juergen at mpi-sb.mpg.de> wrote:
> > while playing with a Scheme-like promise/delay/force mechanism,
> > I had the problem that the two X in the definition 
> > 
> > delay( X ) = promise( (func) = X ).
> > 
> > of delay/1 were considered to be distinct variables by the compiler:
> 
> This is actually a somewhat subtle issue.  It's not clear exactly when
> variables in a pred or func lambda expression should be considered
> fresh variables.  The language reference manual doesn't say anything
> about that (which is certainly a bug), and I'm not sure from a language
> design point of view what the best approach is.
> 
> Consider the following example:
> 
> 	p(A, B, C, P) :-
> 		q(A, B, C),
> 		P = (pred(A::in, B::in, C::out) is semidet :- A+B=C).
> 
> Should the variables A, B, C in the last line be distinct from
> the ones in the first two lines?

In this case it seems pretty clear to me that they should.  I read the
last goal as something like:  "P is the predicate that implements the
relation `for all A, B, C, it's the case that A + B = C'."

> 
> If so, what about this example:
> 
> 	p(A, B, C, P) :-
> 		q(A, B, C),
> 		P = (func(A::in, B::out) = (C::in) is semidet :- A+B=C).

Yes, I agree this question is harder, because the intuition about
functions written in a sort of relational form is not well developed.
My intuition is basically that any variables appearing in "the thing
being defined" should be scoped to the definition (to do otherwise
really makes no sense), while other variables appearing in the
definition should be scoped to the larger clause (to scope them
tighter than that would be too restrictive, making closures pretty
much useless).  In this case, the problem is that "the thing being
defined" at first would appear to be func(A,B), but on closer
examination seems to be forced to be func(A,B) = C.  This view is
unfortunate because cases like the one originally reported become
clumsier than they should be.

The difficulty for me is that I'd like to be able to write things like

	C = ...,
	Addconst = (func(A) = A+C)

If I correctly understand the types/modes problem presented by
closures, Mercury can't support this, because I must include modes and
determinism for the func.  Is that right?  If so, then I'll always
have to write

	Addconst = (func(A::in) = B::out is det :- B = A+C)

and so the rule that says that all variables appearing left of the
`:-' are scoped to the closure is natural enough.  However, if I can
write 

	Addconst = (func(A) = A+C)

as I would much prefer, then this rule doesn't work.  In this case the
intuitive rule (to me) is more complicated: If there is a `:-' in a
func closure, then variables appearing left of it are scoped to the
closure; otherwise, variables appearing left of the `=' are scoped to
the closure.

> Perhaps we should just say that variables in a lambda expression
> are *never* distinct from variables occurring outside; that would
> mean that if you want a fresh variable, then you must use a
> different variable name.

That's a pretty unnatural rule for both preds *and* funcs.  It'll
probably bite people less often than the current rule (because people
will naturally tend to use different variable names for head variables
in closures), so perhaps it's an improvement.  Still, despite the
greater complication, the second scoping rule for funcs I suggested
just above seems more intuitive and less error prone.  If that rule
seems too complicated to you, I suppose an alternative intuition is
that, in a function, `:-' is pronounced `where', and so "the thing
being defined" is always what's left of the `=', and everything right
of the `=' is scoped to the enclosing clause.  In your second example
above this might not do what is wanted, but that one does seem to be a
pathological case.


-- 
Peter Schachte                     In matters of principle, stand like a
mailto:schachte at cs.mu.OZ.AU        rock; in matters of taste, swim with the
http://www.cs.mu.oz.au/~schachte/  current.
PGP: finger schachte at 128.250.37.3      -- Thomas Jefferson