[Haskell-cafe] Slightly off-topic: Lambda calculus

[Andrew Coppin]

Andrew Coppin wrote:
> Well anyway, the obvious thing to do is after each reduction, strip 
> off all the variable indicies and rerun the labeller to assign new 
> indicies. But does this solution work properly in general?

No.

Supposing some Lambda expression eventually reduces to, say,

  \x1 -> \x2 -> x1 x2

Now strip off all the indicies:

  \x -> \x -> x x

...and recompute them...

  \x1 -> \x2 -> x2 x2

FAIL.

To make it worth properly, I would have to (at least) make the renamer 
respect any indicies which are already present. It's nontrivial, but 
doable. Of course, the £1,643,264 question is... would it work even then?