同一シンボルに対して、Withで束縛する場合の動作が一貫していないように見えます

例題として
With[{val = foo},
Scan[With[{val = #}, Print[ToString[val]]]&, {1, 2, val, 3, 4}]];
を考えます。ここで、内側のWithで束縛される valは Scan[]に与えた純関数スコープで閉じています。

期待される出力は、
1
2
foo
3
4
となります

ここで、fooに NaNを設定した式
With[{val = NaN},
Scan[With[{val = #}, Print[ToString[val]]]&, {1, 2, val, 3, 4}]];
を評価すると出力は
NaN
NaN
NaN
NaN
NaN
となり、内側のWithによる valの再束縛に失敗しているように見えます

> 同一シンボルに対して、Withで束縛する場合の動作が一貫していないように見えます
>
> 例題として
> With[{val = foo},
> Scan[With[{val = #}, Print[ToString[val]]]&, {1, 2, val, 3, 4}]];
> を考えます。ここで、内側のWithで束縛される valは Scan[]に与えた純関数スコープで閉じています。
>
> 期待される出力は、
> 1
> 2
> foo
> 3
> 4
> となります
>
> ここで、fooに NaNを設定した式
> With[{val = NaN},
> Scan[With[{val = #}, Print[ToString[val]]]&, {1, 2, val, 3, 4}]];
> を評価すると出力は
> NaN
> NaN
> NaN
> NaN
> NaN
> となり、内側のWithによる valの再束縛に失敗しているように見えます
>
内部解析の結果、これは Replace[]の影響と判明しました(*1)

Real型に対する比較の実装が、IEEE754の算術比較なので NaN同士が同値にならないため
次のようになります
{1, NaN, 3}/.{1->2} -> {2, NaN, 3}
{1 ,NaN, 3}/.{NaN->2} -> {1, NaN, 3}

したがって、With束縛にReplaceの内部実装を流用しているので、上記の Withの問題は
With[{val = NaN}, Scan[With[{val = #}, Print[ToString[val]]]&, {1, 2, val, 3, 4}]];
-> Scan[With[{NaN = #}, Print[ToString[NaN]]]&, {1, 2, NaN, 3, 4}];
と変換されたあとに、局所シンボル NaNの置換が失敗していることになります

(*1)に対するパッチは開発済みで、上記の問題は解決するのですが、With束縛自身に次の問題があることが分かりました

次のコードの振る舞いを考えてみてください
f = With[{val = #}, Print[ToString[1 + val]]]&;
With[{val = 1},
Scan[f, {1, 2, val, 3, 4}];
];
上記コード中の シンボル fに束縛される純関数を即値形式にした式
With[{val = 1},
Scan[With[{val = #}, Print[ToString[1 + val]]]&, {1, 2, val, 3, 4}];
];
は動作が変わってしまいます
同様に、
f = With[{val = #}, Print[ToString[1 + val]]]&;
With[{f, val = 1},
Scan[f, {1, 2, val, 3, 4}];
];
と
f = With[{val = #}, Print[ToString[1 + val]]]&;
With[{f}, With[{val = 1},
Scan[f, {1, 2, val, 3, 4}];
]];
でも動作が変わります

Withによつ局所シンボル束縛が、内側のWith局所シンボルスコープまで作用していることが事の本質のようですが、
これは意図された仕様なのでしょうか？

純関数の中でWithを使う意図としては、シンボルを局所拘束して外部との干渉を避けることが目的ですが、
現行のWithの動作はこれを破壊してしまいます。

この問題は、Functionも含めてk64-1-6で対応が試みられています。

With[{a=2}, With[{a=3}, ...]]

のように、Withのlocal symbolがかぶる場合、内側のsymbolが優先します。ただし、

With[{a=2}, With[{a}, ...]]

のように、内側のsymbolの値を与えない場合は、内側のsymbol aを外側のWithの置換対象にしています。要議論です。

Functionの場合は常に内側が優先します。

> この問題は、Functionも含めてk64-1-6で対応が試みられています。
>
> With[{a=2}, With[{a=3}, ...]]
>
> のように、Withのlocal symbolがかぶる場合、内側のsymbolが優先します。ただし、
>
> With[{a=2}, With[{a}, ...]]
>
> のように、内側のsymbolの値を与えない場合は、内側のsymbol aを外側のWithの置換対象にしています。要議論です。
>
> Functionの場合は常に内側が優先します。
>
With[{a = 2}, With[{a}, ...]]の解釈ですが、
With[{a}. ...]は、式(...)中の aを aの評価値(つまり、当該With環境の外で aに拘束された値)と置換するので、
冗長な記述をすると With[{a = a}, ...]に等価になると思います

したがって、シンボルスコープを含めて書き下すと
With[{a = 2}, With[{a}, ...]] -> With[{a$1 = 2}, With[{a$2 = a$1}, ....]]
となるべきだと思います

同じようなスコープ解決問題として、With[{a = 3}, With[{a = a + 2}, a]]の評価値は
(2+a)ではなく 5を返すべきだと思います
2012-07-20 11:18 checkoutのソースだと (2+a)を返します

スコープ解決
With[{a = 3}, With[{a = a + 2}, a]]
-> With[{a$1 = 3}, With[{a$2 = a$1 + 2}, a$2]]

仰る通りです。解決法としては、Moduleのような世代番号好きのlocal symbol を使う手もありますが。少しコストが高いのと、終了後に消去する手間がかかる、ということで、置換のみで対応したい気持ちです。

一応、対策を施しましたが、完全ではないと思います。