Quantification expressions should have their own name scope

[sadboy]

Currently, a quantification expression does not introduce a name scope, which means any variables bound by the expression is "pass through" to the parent scope. The original consideration was to simplify witness binding. For example,

class P(process):
    def setup():
        self.n = 1

    def run():
        some(n in [1, 2], q in [2, 3])
        output(n, q)

the existential quantification in P.run() will bind q in the local scope of run, but will also bind the process-level `n``. The latter behavior which would be counter-intuitive, and runs contrary to Python's binding rules for comprehensions.

[yanhongliu]

Right, but note that the former is bad too, and Python 3 does not do that. That's my point last Thursday---it's independent of whether there is an implicit "self". For example:

>> [i for i in range(10)]

[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

>> i

Traceback (most recent call last): File "<stdin>", line 1, in <module> NameError: name 'i' is not defined

>> i = 0 >> [i for i in range(10)]

[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

>> i

0

…

On Sun, Jun 25, 2017 at 11:36 AM, Bo Lin ***@***.***> wrote: Currently, a quantification expression does not introduce a name scope, which means any variables bound by the expression is "pass through" to the parent scope. The original consideration was to simplify witness binding. For example, class P(process): def setup(): self.n = 1 def run(): some(n in [1, 2], q in [2, 3]) output(n, q) the existential quantification in P.run() will bind q in the local scope of run, but will also bind the process-level `n``. The latter behavior which would be counter-intuitive, and runs contrary to Python's binding rules for comprehensions. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#10>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AIb1-aozUVJerIlGXuW0r3XGWIzPXo9xks5sHn52gaJpZM4OEo4x> .

[sadboy]

Right, but note that the former is bad too, and Python 3 does not do that.

But the former is DistAlgo's witness binding semantics for existential quantifications.

[yanhongliu]

Back to this: indeed, we had decided that the scope for "some" is the
method/function scope here (and, in general, the smallest block scope
in the host language being extended, which is the entire function here
because Python has no smaller block scopes; this way, we don't have to
write anything special about the scope of these variables).

So there are two ways to interpret your example:

1. any use (read/write) of n in "run" is on the process-local n, same
   as uses of process-local variables in general, so "some" writes to
   that "n". this is the current implementation.
2. the scope of n from "some" is the entire "run", so in "run", use of
   n refers to the n bound by "some", but one could still allow the use
   of "self.n" to refer to the process-local n.

In a richer language with block scopes, "some" could have smaller
scopes, e.g., in
if some(x in range(10), has= x*x>80 ): print(x)
x could be local to only the if- branch. this is more consistent with 2 above.

however, in general, nested local scopes need more effort to
implement. they also make code more complicated and harder to read.
so i'm not eager to add them.

in the special case of "some", it could be worthwhile to add, and
might even be a best use of nested scopes, but i'd wait until we see
such sophisticated uses that really justify adding.

so for now at least, the current implementation for Python is ok.