functions - Is the renaming mechanism of `With` flawed?

I'm confused about the renaming mechanism of With:

With[{x = a}, Hold[With[{a = b}, a + 2 x]]]
(*==>Hold[With[{a$ = b}, a$ + 2 a]]*)

With[{x = a$}, Hold[With[{a = b}, a + 2 x]]]
(*==>Hold[With[{a$ = b}, a$ + 2 a$]]*)

The documentation tells us that

With constructs can be nested in any way, with inner variables being renamed if necessary.

There is name conflict in the first case, so renaming is quite reasonable. However, in the second case, there is no name conflict at all, why Mathematica renames a to a$?

I've checked some simple cases which all show that With does the renaming work simply by appending $ to var (with the exception that var ending with only one $ is untouched):

With[{x = a}, Hold[With[{aa$ = b}, aa$ + 2 x]]]
(*==>Hold[With[{aa$ = b}, aa$ + 2 a]]*)

With[{x = a}, Hold[With[{aa$$ = b}, aa$$ + 2 x]]]
(*==>Hold[With[{aa$$$ = b}, aa$$$ + 2 a]]*)

If this is really the underlying renaming mechanism, IMHO, this will be dangerous.

As can be seen from the second case, one can deliberately constructs some names ending with $, and the results will vastly change.

Specifically, if we have a program involving With, the result of

With[{x=var1$},...blackBoxCode...]

may be totally different from

With[{x=var2$},...blackBoxCode...].

To summarize, my questions are the following three,

1. 
   
   

   Do symbols ending with $ have some special meanings?

   
   


2. 
   

   Why With renames variables when there is no name conflict at all?

   
   


3. 
   

   Is the renaming mechanism of With flawed?

   
   

Answer

Short answer

1. 
   

   The local variables of the form varname$... are used by the system, and it is unwise to use symbols with such names as local variables.

   
   


2. 
   

   With, like many other lexical scoping constructs, performs excessive renamings, often even in cases where it isn't strictly necessary. This probably has to do with efficiency - full analysis may be more costly.

   
   


3. 
   

   Yes, the renaming mechanism is fundamentally flawed, and can be broken, deliberately (as in your example), or accidentally. This doesn't make it unusable though - to avoid most of the issues, one just needs to be careful and avoid certain bad practices.

   
   
   

Longer answer

The crux of the matter

It is important to realize what is the fundamental problem here. That is a problem of emulating lexical scoping with variable renamings.

Here are the core requirements to the lexical scoping, that most modern programming languages satisfy:

• 
  

  Encapsulation

  
  

  This means that the local lexical variables are inaccessible to the code outside the scope

  
  
  


• 
  

  Locality and chained lexical environments

  
  

  This means that the code inside inner lexical scoping constructs has access to outer scopes.

  
  


• 
  

  Ability to create closures

  
  

  This means that one can create functions, or delayed code thunks, which would have an access to a given lexical scoping environment (set of local variables, roughly speaking), even after the code execution left that scope.

  
  

  This also means that the outer scopes should be available to such code (closures) as well, if it was referenced by the inner scope when that one was constructed.

  
  

In many other languages (for example, Scheme, javascript, R, etc.), the way these requirements are fulfilled is through local lexical environments. Basically, each environment has a pointer to it, and keeps pointers to outer environments, but otherwise is completely closed and encapsulated. In such a case, encapsulation is complete, because there is absolutely no way to break it from the outside.

The problem of colliding variable names at different scoping levels (which is the main reason for the renaming mechanism in Mathematica to exist), is solved in such a case simply by construction - the inner variables shadow the outer ones automatically, due to the way variable lookup is performed. This is because, in such a case, the environments are truly nested, and the variable lookup is done from inner to outer scopes. At any given time, only one scope is searched for a variable, and within single scope variables are always unique.

In Mathematica, things are different. The main reason is its "overtransparent" nature, where everything is an expression to the extent that the user is free to manipulate even scoping constructs with rules and patterns. This can be also seen in the way function calls are performed, and associated argument-passing: instead of the more standard mechanism where each function gets a stack frame where passed parameters are copied as local variables, in Mathematica functions all work like macros: they are essentially placeholders, and the parameters are injected verbatim into the body of the function, before it starts executing.

Because of this, the level of encapsulation and the more standard approach to implementing lexical scoping would fly in the face of such transparency, making lexical scoping constructs inaccessible for destructuring and pattern-matching. So, my guess is that it was a conscious design decision to keep things open and playing well with the core principles of the language.

But then, you can't have local closed environments, so pretty much the only simple choice you have is to emulate it with one big environment (it might be possible to reconcile the open nature of Mathematica expressions with nested scopes somehow, but that seems a much more complex problem, and would probably require introducing new constructs and primitives into the language). Since you have one big environment, you can't really easily form a hierarchical lookup mechanism used in other languages. Therefore, you have to worry about variable collisions, and do something about that. Hence the variable renaming mechanism.

The dangers of variable renaming mechanism

There are basically three distinct ways in which renaming mechanism can be broken in Mathematica

1. 
   
   

   Deliberate or accidental breaking by the user, who happens to use variables that have a high chance to collide with those produced by renaming mechanism

   
   

   This can be easily avoided with some minimal discipline - you basically should not use variables like varname$... for your local variables.

   
   


2. 
   

   Persisting code involving such local variables in one session (e.g. via Save or DumpSave), and loading it into another session.

   
   

   This has to do with the fact that the variables are only guaranteed to be unique in a given Mathematica session. If you know about this and avoid this, you should be fine

   
   


3. 
   

   The system itself may not work properly in some cases. There are a number of such, but the most serious problem is arguably described here:

   
   

   f[x_] := g[Function[a, x]];
   
   g[fn_] := Module[{h}, h[a_] := fn[a]; h[0]];
   f[999]
   

   
   

   and is pretty bad because this makes passing around Functions with named variable infeasible.

   
   

This last set of issues can be cured (thanks to Daniel Lichtblau), with a recently added system option "StrictLexicalScoping", which one has to set to True.

The ways out

The described issues are certainly serious, but in my view, they don't make the lexical scoping in Mathematica unusable. One just has to follow certain guidelines, some of which I mentioned above:

• 
  

  Don't name your local variables like varname$...

  
  


• 
  

  Don't persist code involving local variables between Mathematica sessions

  
  

These simple rules will cover the majority of problematic cases. For the rest of them, I can suggest two alternatives

1. 
   
   

   Use the "StrictLexicalScoping" system option. For example:

   
   

   SetSystemOptions["StrictLexicalScoping" -> True];
   With[{x = a}, Hold[With[{a = b}, a + 2 x]]]
   With[{x = a$}, Hold[With[{a = b}, a + 2 x]]]
   
   (* 
    Hold[With[{a$1121237 = b}, a$1121237 + 2 a]]
   
    Hold[With[{a$1121239 = b}, a$1121239 + 2 a$]]
   *)
   
   



2. 
   

   Some years ago I wrote a tiny micro-framework to deal with renamings, which lives here. Here is how one can use it:

   
   

   SetSystemOptions["StrictLexicalScoping" -> False]
   Import["https://gist.githubusercontent.com/lshifr/1683497/raw/AutoRenamings"]
   

   
   

   And now:

   
   

   runWithRenamings[With[{x = a}, Hold[With[{a = b}, a + 2 x]]]]
   runWithRenamings[With[{x = a$}, Hold[With[{a = b}, a + 2 x]]]]
   
   
   (*
   
    Hold[With[{a$1121244$ = b}, a$1121244$ + 2 a]]
   
    Hold[With[{a$1121075$ = b}, a$1121075$ + 2 a$]]
   *)
   

Summary

The problem indeed does exist. I view it as a (perhaps anavoidable) consequence of the transparent nature of Mathematica expressions, and the design decision to expose lexical scoping constructs to the user as Mathematica expressions.

This has both upsides and downsides. The upside is that one can do a lot of things which would be hard to do in languages where scoping constructs are less accessible. The downside is that lexical scoping is not fully robust and one needs to be extra careful to avoid problems.

Still, there are ways to minimize the risks, and some of these rules are pretty simple. This does, however, require some extra knowledge on the part of the user, and may come as a surprise for uninitiated.