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?

• closely related recent discussion in chat: chat.stackexchange.com/transcript/message/30555061#30555061
– Kuba
Jun 26 '16 at 12:24
• @Kuba It helps to know that Set also does the renaming stuff. I'm more confident about the guess in my OP. However, still I insist that this renaming is somewhat too naive and dangerous. With this renaming mechanism at hand, for the example in the chat given by Szabolcs (from the documentation) , one can make it work by makedef[x$] and then f will work as expected. Jun 26 '16 at 13:01 • @luyuwuli I would do something like With[{x = a$}, Hold[With[{Hold[Set][a, b]}, a + 2 x]]] /. Hold[Set] -> Set /. Hold -> Identity. And yes, With is not smart at all and the documentation is not clear ("if necessary" is not very specific). Jun 26 '16 at 13:12
• Related, I believe: (20766), (42351), (72758), (91917) Jul 8 '16 at 10:08

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];
f

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. • Thanks. I still need some time to digest. However, as a quick comment. My first question is variables ending with$ other than starting with $. Jun 26 '16 at 13:52 • This is so detailed and helpful that I cannot simply go away without leaving a grand "thanks!" to you! – Wjx Jun 26 '16 at 13:56 • @luyuwuli Actually, I made a mistake - I meant not using$ in the fashion varname$123. I will correct the text. Jun 26 '16 at 14:01 • I'm not sure whether I'm correct: except that With forces one to do initialization and it literally replaces variables (outside some other scoping structure) before evaluating the body, With is the same as Module. If StrictLexicalScoping is turned off, the renaming is quite flawed, simply appends variables with$; if turned on, it do the renaming by avoiding name collision just like what Module does. Or in short, With+StrictLexicalScoping= With + safer names. Jun 26 '16 at 14:38
• @luyuwuli This sounds correct, but "StrictLexicalScoping" does more than that, and not only for With. I don't really know the details of how it works, the right person to ask is Daniel. However, in some sense, the whole point here is that we don't really want to know these details. Jun 26 '16 at 14:45