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 "", line 1, in 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 notifications@github.com 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 https://github.com/DistAlgo/distalgo/issues/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.