First of all, thanks for reading my proposal, and I apologize for the ill-considered rant which preceded it. I hope you won't hold it against me -- we should all be on the same side here. On Sun, 3 Aug 2003, Ashley Yakeley wrote:
((let g = \_ _ -> \@x -> @x in ((g (\@x -> @x)) {@x = 2})) (\@x -> @x)){@x = 1} ((let g = \_ _ -> \@x -> @x in (g 2)) (\@x -> @x)){@x = 1}
This reduction is incorrect. Auto-lifted parameters on the RHS of an application get lifted out, so g (\@x -> @x) => (\@x -> g { @x = @x } @x) Therefore g (\@x -> @x) { @x = 2 } => (\@x -> g { @x = @x } @x) { @x = 2 } => g { @x = 2 } 2, not (g 2) as you wrote. Several of the other steps in your reductions are incorrect for the same reason. I think the following is a correct reduction, although it's easy to get them wrong when you do them by hand: let ?x = 1 in ((let g = \_ _ -> ?x in let ?x = 2 in g ?x) ?x) => ((let g = \_ _ -> ?x in g ?x {?x=2} ) ?x) {?x=1} => ((let g = \_ _ @x -> @x in g (\@x -> @x) {@x=2} ) (\@x -> @x)) {@x=1} => (\_ _ @x -> @x) (\@x -> @x) {@x=2} (\@x -> @x) {@x=1} => (\@x -> (\_ _ @x -> @x) { @x = @x } @x) {@x=2} (\@x -> @x) {@x=1} => (\_ _ @x -> @x) {@x=2} 2 (\@x -> @x) {@x=1} => (\_ _ -> 2) 2 (\@x -> @x) {@x=1} => (\_ -> 2) (\@x -> @x) {@x=1} => (\@x -> (\_ -> 2) @x) {@x=1} => (\_ -> 2) 1 => 2 This is the answer I expected intuitively. If you can produce a correct reduction which yields anything else, then I'll concede defeat. (For now.)
[?x,?x] {@x=1} -- OK [?x] {@x=1} -- OK [] {@x=1} -- not OK
Interesting. Can you give an example of this problem cropping up in a more realistic context? Certainly no one will write "[] {@x=1}", since either it's an error or it's exactly equivalent to "[]". My intuition is that this is a minor problem which would bite very rarely in practice, like "show []". And, let me emphasize again, it's safe: programs will not silently behave in an unexpected way because of this. By the way, I respectfully disagree that requiring explicit ?x bindings to be used is ugly. It's an ugly additional rule in the current framework, which treats implicit parameters as a way of simulating a Lisp-like dynamic environment, but it's the natural state of affairs in my proposal, which treats implicit parameters as parameters. In my proposal it's ugly /not/ to require explicit ?x bindings to be used -- it would be like defining (f x) to be f when f is not a function. -- Ben