0000169: Lambda predicates do not allow references to existing variables in the head

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000169

mercury

Bug

public

2010-11-15 13:57

Reporter

mgiuca

Assigned To

Priority

normal

Severity

minor

Reproducibility

always

Status

new

Resolution

open

Product Version

Target Version

Fixed in Version

Summary

0000169: Lambda predicates do not allow references to existing variables in the head

Description

I am not sure if this is a bug, or intentional, and if it is not intentional, I'm not sure whether it is worth "fixing", but I'll report it anyway.

The terminology I'm using is from section 2.8 (Rules) of the Mercury reference, where a function is defined as "Head = Result :- Body" and a predicate as "Head :- Body".

There seems to be an inconsistency with the way lambda predicates treat variable scoping. The compiler seems to scope variables with the following rules (for both lambda functions and lambda predicates):
1. Any name which appears in the Result and/or Body of a lambda term but not at all in the scope outside of the lambda is scoped locally to the lambda term.
2. Any name which appears in the Head of a lambda term is also scoped locally to the lambda term (and if it also appears in the scope outside the lambda, is treated as a distinct variable, shadowing the one outside).
3. Any name which does not appear in the Head, but does appear in the scope outside, is scoped to the closure outside the lambda term.

This basically mirrors the laws of lambda abstraction in the lambda calculus: variables appearing in the head are "bound" to the abstraction (and shadow other variables with the same name outside); variables not appearing in the head are "free" in the abstraction, and depend upon the name existing in an outer scope.

It means that code like this functions as expected:

:- pred add_list(int::in, list(int)::in, list(int)::out) is det.
add_list(X, L0, L) :-
    list.map((pred(A::in, B::out) is det :- B = A + X),
             L0, L).

Note the name X, which is scoped to the add_list predicate, appears in the Body of the lambda pred, referring to the same variable X.

However, rule 0000002 above doesn't make a lot of sense considering the semantics of predicates. Any data term appearing in the body of a predicate should have the same meaning if moved to the predicate's head. So the following definition should be equivalent:

:- pred add_list(int::in, list(int)::in, list(int)::out) is det.
add_list(X, L0, L) :-
    list.map((pred(A::in, A + X::out) is det), L0, L).

All I have done is replace the Head variable B (unified with A + X in the Body) with the expression A + X, directly in the Head. This produces the following compiler error:

In clause for predicate `lambdahead.add_list2'/3:
  warning: variable `X' occurs only once in this scope.
In clause for predicate `lambdahead.add_list2'/3:
  warning: variable `X' occurs only once in this scope.
In clause for `add_list2(in, in, out)':
in call to function `int.+'/2:
mode error: arguments `A, X, V_9' have the following insts:
   ground,
   free,
   free
which does not match any of the modes for function
`int.+'/2.

Basically, the fact that X now appears in the lambda's Head makes the lambda predicate treat it as a distinct variable to the outer-scoped variable also called X (as it would in the lambda calculus). The error message tells me that the two separate variables "X" each appear only one time, and that I am trying to do arithmetic on an unbound variable.

It is difficult to see how to properly "fix" this situation, if indeed it is considered to be broken. I would recommend changing the rule for lambda predicates (but not functions) such that variables appearing in the Head have the same scoping rules as those appearing in the Body -- they do not create a new variable if one already exists in the outer scope. However, this might break some existing code, and would make a new difference between predicates and functions. (The same rule would not make sense applied to functions.) So I acknowledge that it is a pretty difficult situation.

Although it might break existing code, it would always be possible for new code to be right: simply don't shadow existing variable names in lambda predicates.

Note that it would help if the reference manual made a mention of this rule. I can't find it in "Rules", "Variable scoping" or "Creating higher-order terms", which are the obvious places to look.

Date Modified	Username	Field
Issue History
2010-11-15 13:57	mgiuca	New Issue
2010-11-15 13:57	mgiuca	File Added: lambdahead.m

Relationships