Is Mathematica's lexical scoping broken?

Why do these two lines output different things (b and 0, respectively)? Is it a bug?

ReleaseHold@With[{a=0},FlattenAt[Map[List,FlattenAt[Hold@With[{b=0,b=b},b+0a],{1,1}],{2}],{1,-1}]]
ReleaseHold@With[{a=0},FlattenAt[Map[List,FlattenAt[Hold@With[{b=0,b=b},b+0b],{1,1}],{2}],{1,-1}]]


(Sorry, I couldn't find a shorter example that didn't give an error.)

Just wanted to post back 3 years later to dissect what's happening.

tl;dr: It's a broken (sorta-lexical, sorta-dynamic, sorta-syntactic) substitution. If you really want lexical scoping, Module may be closer to what you want, although it's not clear to me that even Module (or anything else) could possibly do it perfectly.

To see what's happening, here's the same code, echoing every step:

(Edit: Renamed the second b to c to avoid a duplicate variable as suggested in the comments.)

In[1]:= Module[{x},
With[{a = 0},
x = Echo[Hold[With[{b = 0, c = b}, c + 0 a]]];
x = Echo[FlattenAt[x, {1, 1}]];
x = Echo[Map[List, x, {2}]];
x = Echo[FlattenAt[x, {1, -1}]];
ReleaseHold[x]]]

>> Hold[With[{b$$=0,c$$=b},c$+0 0]] >> Hold[With[b$$=0,c$$=b,c$+0 0]]

>> Hold[With[{b$$=0},{c=b},{c$$+0 0}]]

>> Hold[With[{b$$=0},{c=b},c$$+0 0]]

Out[1]= b


Here's what happens if we change 0 a to 0 b (or in fact, 0 followed by any other variable):

In[2]:= Module[{x},
With[{a = 0},
x = Echo[Hold[With[{b = 0, c = b}, c + 0 b]]];
x = Echo[FlattenAt[x, {1, 1}]];
x = Echo[Map[List, x, {2}]];
x = Echo[FlattenAt[x, {1, -1}]];
ReleaseHold[x]]]

>> Hold[With[{b=0,c=b},0 b+c]]

>> Hold[With[b=0,c=b,0 b+c]]

>> Hold[With[{b=0},{c=b},{0 b+c}]]

>> Hold[With[{b=0},{c=b},0 b+c]]

Out[2]= 0


What seems to be happening here is that Mathematica only attempts to figure out the scope of a variable once it is forced to actually manipulate the expression containing it semantically. In this case, that means the semantic substitution of a=0 in the inner expression is triggering variable renaming, which is how Mathematica resolves naming conflicts. If that doesn't ever happen, then the engine doesn't bother to resolve name conflicts at all.

So after the ReleaseHold, what we're left with are these two expressions to evaluate:

With[{b$$= 0}, {c = b}, c$$]
With[{b  = 0}, {c  = b}, c ]


This is actually a "sequential With" that is highlighted poorly, but equivalent to the following:

With[{b$$= 0}, With[{c = b}, c$$]]
With[{b  = 0}, With[{c  = b}, c ]]


In the first case, the outer c\$ = 0 has no effect on the innermost expression, since it is hidden ("shadowed") by the inner one. In the second case, this is also true, but the 0 value of b is substituted into c before b is hidden. Thus in the first case we're left with the unbound symbol b, whereas in the second case it simplifies down to 0.

The thing is, this is wildly broken behavior, because lexical scope is a static property, whereas Mathematica triggers it dynamically. Note that whether Mathematica decides to resolve naming conflicts via renaming or via tracking them internally (like most other languages) isn't relevant to this—they're just implementation details. The important thing is that expressions maintain their semantics, and that requires that a variable like c refers to the same thing regardless of whether it is later added to 0 a or 0 b.

Then why does Mathematica do this?

Because the language specification is self-contradictory. Specifically (not sure if pun intended):

• With is a scoping construct that implements read-only lexical variables.
With replaces symbols in expr only when they do not occur as local variables inside scoping constructs.

• With[{x=x0,y=y0,…},expr] specifies that all occurrences of the symbols x, y, … in expr should be replaced by x0, y0, ….

At first glance these seem fine, but in fact these two requirements point to a deep inconsistency in how Mathematica treats expressions, stemming from a lack of a clear separation between static and dynamic properties of code.

Namely, the first specification is a semantic requirement, and thus requires static semantic analysis of expr. For Mathematica to implement "lexical scope" and understand that it should not replace a nested local variable, it needs to be able to identify each With, Module, etc. construct in the first place. However, this is impossible inside constructs like Hold, because Mathematica is so dynamic that it allows you to construct expressions at runtime. For example, compare the following two statements:

    ReleaseHold[With[{x = 0}, Hold[With [{x = 1}, x]]]] (* OK?!?! *)
With2 = With;
ReleaseHold[With[{x = 0}, Hold[With2[{x = 1}, x]]]] (* error! *)


You'd expect them to be semantically equivalent, except that it is impossible for Mathematica to know whether a given expression is a With construct without actually evaluating it. (A With might be something else initially, like Symbol["With"], or, conversely, the user might have wanted to later replace a With with something else.)

The second specification acknowledges as much. It admits that in fact the language is performing a symbolic (syntactic) substitution, not a semantic one. And that implies, by its definition, that With does not implement lexical scoping.

Instead, what With really does is that it fakes a semantic pre-analysis: it pretends that the language isn't dynamic at all, assumes that any With expression will look like With[...] (rather than, say, With2[...] above), and then performs the substitution hoping that you don't notice any discrepancy.

Admittedly, in practice, it works fine, because people rarely write expressions whose meanings are extremely dynamic, and thus preserve the static meanings of symbols—otherwise, it becomes harder for people to read such code, too. But it's a fundamentally conflicting language requirement to attempt to statically substitute inside what can be a completely dynamic expression, and there isn't really a true fix for it. The best they can do, therefore, is to fix the documentation and explain precisely what really happens (a half-baked mishmash of symbolic/static/dynamic substitution, with a trigger of variable renaming that can suddenly change the semantics of the inner expression unexpectedly!), as opposed to what they're trying to fake (lexical scoping).

• I fail to see how this is anything other than undefined behavior.If there is a bug, it is that With did not give an error when a variable appeared twice in the lhs of the assignment list. – Daniel Lichtblau Aug 18 at 13:38
• This variant might be a better example. In that inner With change the second variable. With[{b = 0, c = b}, c + 0 b] vs. With[{b = 0, c = b}, c + 0 a] – Daniel Lichtblau Aug 18 at 13:44
• @DanielLichtblau: Thanks, I changed it to clarify. But I disagree that it's undefined behavior. There's a Hold outside which prevents its evaluation, and undefined behavior only occurs when a behavior is demanded of the expression -- that is, during evaluation. That makes it equivalent to Hold[With[{a=1,a=2},a]], which doesn't (and shouldn't) give an error. – Mehrdad Aug 18 at 16:06
• @Daniel: actually.... this is giving me second thoughts. Maybe that should also be an error? It's weird because Mathematica is both trying to analyze the expression and also avoid doing so. It might be outright impossible to give it reasonable semantics at all -- I'll write more when I have a chance (maybe in another 3 years? haha). – Mehrdad Aug 18 at 16:32
• With the change to use c instead of b it could well be a scoping bug, I'm not sure. Possibly the lexical scoping emulation should always rewrite. The business of using b both as lhs and rhs of With assignments makes it a bit hard for me to determine what to expect for when rewriting will or will not happen. – Daniel Lichtblau Aug 19 at 2:47

[Too long for a comment but not a full response.]

I am starting to see this differently. Sequential With assignment lists (which I realize are not yet documented) can behave differently from the flat counterpart, when a symbol appears both as an lhs and rhs. In particular these will behave differently.

With[{b = 0}, {c = b}, c + 0 b] // Trace // InputForm

(* Out[2713]//InputForm=
{HoldForm[With[{b = 0}, {c = b}, c + 0*b]], HoldForm[With[{c$$= 0}, c$$ + 0*0]],
HoldForm[0 + 0*0], {HoldForm[0*0], HoldForm[0]}, HoldForm[0 + 0], HoldForm[0]} *)


I think there is no controversy here.

With[{b = 0, c = b}, c + 0 b] // Trace // InputForm

(* Out[2714]//InputForm=
{HoldForm[With[{b = 0, c = b}, c + 0*b]], HoldForm[b + 0*0],
{HoldForm[0*0], HoldForm[0]}, HoldForm[b + 0], HoldForm[b]} *)


This much is as designed: With assignments only apply to later arguments so the b in that c=b assignment does not get lexically replaced.

Using Hold as in the original examples delays some of the evaluation, in a way that I think is also not controversial. Since the original With argument list has been split at that point, I am inclined to see the eventual behavior as also being according to design.

Now for the renaming, I am again not sure anything is amiss. Here are two examples to show what I have in mind. In the first we see the inner With variables get renamed.

Trace[With[{a = 0}, x = With[{b = 0, c = b}, c + 0 a]]] // InputForm

(* Out[2723]//InputForm=
{HoldForm[With[{a = 0}, x = With[{b = 0, c = b}, c + 0*a]]],
HoldForm[x = With[{b$$= 0, c$$ = b}, c$$+ 0*0]], {HoldForm[With[{b = 0, c = b}, c$$ + 0*0]], HoldForm[b + 0*0],
{HoldForm[0*0], HoldForm[0]}, HoldForm[b + 0], HoldForm[b]}, HoldForm[x = b],
HoldForm[b]} *)


In this next case we do not rename With variables.

Trace[With[{a = 0}, x = With[{b = 0, c = b}, c + 0 b]]] // InputForm

(* Out[2724]//InputForm=
{HoldForm[With[{a = 0}, x = With[{b = 0, c = b}, c + 0*b]]],
HoldForm[x = With[{b = 0, c = b}, c + 0*b]],
{HoldForm[With[{b = 0, c = b}, c + 0*b]], HoldForm[b + 0*0],
{HoldForm[0*0], HoldForm[0]}, HoldForm[b + 0], HoldForm[b]}, HoldForm[x = b],
HoldForm[b]} *)


The salient difference between these and the held examples is that the held ones gave rise to a split in the With` assignment lists, and that does allow for different semantics than the unsplit case. It happened in such a way that it was affected by whether or not renaming took place.

As I mentioned in a comment, I suppose one way to address this would be to force variable renaming to always happen. Not sure how popular such a change would be though.

• Comments are not for extended discussion; this conversation has been moved to chat. – Kuba Aug 21 at 6:20