Is Mathematica's lexical scoping broken?

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):

• Specification #1::

  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.

• Specification #2::

  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).

[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.