The madness of implicit parameters: cured?

[Ben Rudiak-Gould]

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