Anyway, Conor and James' Haskell Workshop paper on manipulating syntax that involves both free and bound variables [1] is really nice and could perhaps be of interest to you.
If I remember correctly this paper is not about a pure de Bruijn index representation, but about a mix between names and indices which often goes under the name "locally nameless".
what is sometimes forgotten is that de Bruijn introduced not one, but two numbering schemes. it is interesting that those who actually do the implementations tend to emphasise the importance of both schemes (Berkling was keen on pointing them out, and [1] mentions both on page 2). the better known de Bruijn indices (counting binders from the inside) are useful for local naming in subexpressions, where binders tend to move around, commute, and disappear during reductions. the less known de Bruijn levels (counting binders from the outside) are useful for constant prefixes in contexts, where binders tend to remain stable during reduction of subexpressions. indices are useful for reducing scoping issues to arithmetic, levels are useful for avoiding some of the scoping issues alltogether. if you are implementing transformations without any stable context, indices (or lambda bars) are your friend, if you are implementing transformations within some stable context, you can take references to binders within such context out of the numbers game. McBride and McKinney suggest a nested name scheme for such locally free variables, corresponding to de Bruijn levels; some of Berkling's and Kluge's reduction systems simply ignored such locally free variables during reduction, treating them as constants - if a variable is bound to a binder in the stable context, it will still be bound to the same binder after reductions- and reestablishing the correct presentation during postprocessing, which is straightforward. consider reduction in lambda bodies as an example: \x->(\x->\x->(/x //x)) x -> \x->\x->(/x /x) here, we have three binders for 'x', the first of which is part of a stable context (it will not change during reductions), the second disappears during beta-reduction, and the third is currently part of the active subexpression, but will become part of the stable prefix after reduction. in Haskell, such an expression would have been subject to renaming obfuscation already: \x->(\z0->\q32->(z0 x)) x -> \x->\q32->(x x) the nice thing about de Bruijn indices or Berkling's lambda bars (protection keys) is that they are a local referencing scheme [*], independent of the context in which the subexpression is placed. but if there is a stable binding context, indices involve unnecessary index computations (here the '0' and '2' refer to the same binder in the stable context, but would be updated again and again during reductions): /\.(/\/\(1 2)) 0 -> /\./\(1 1) the nice thing about de Bruijn levels is that references to binders in stable contexts do not involve any computation at all, but for the more common case of binders in the subexpressions being transformed, levels are awkward to use (here, the number used to represent '1' depends not only on the subexpression under reduction, but on the context in which it is situated, so the same subexpression in another context would have a different representation): /\.(/\/\(1 0)) 0 -> /\./\(0 0) the common approach is to use indices or lambda bars as the default, and levels as an optimisation for stable contexts (i'll use '[x]' to represent a locally free variable): \x->(\x->\x->(/x //x)) x -> -- pre-processing \x->(\x->\x->(/x [x])) [x] -> -- reduction/transformation \x->\x->([x] [x]) -> -- post-processing \x->\x->(/x /x) as you can see, neither of the '[x]' needs to take part in the index calculations during reduction/transformation - they are taken out of the game during pre-processing, and put back into the common notation during post-processing. that is because the context they refer to remains stable, and as long as we know they refer to it, we can prevent accidental shadowing in the user-level representation through simple post-processing. hth, claus [*] this was essential for Berkling because he was working on a hardware implementation of lambda calculus reductions, based on a system of three or more stacks, where the three main stacks provided a hardware representation of what is nowadays known as a zipper, enabling the hardware reduction machine to navigate through reduction contexts and to perform reductions locally. some of those old works are now online - see, for instance: Reduction languages for reduction machines, KJ Berkling, International Conference on Computer Architecture Year of Publication: 1974 http://portal.acm.org/citation.cfm?id=642112 Computer employing reduction language, Klaus Berkling, 1978 http://www.google.com/patents?hl=en&lr=&vid=USPAT4075689&id=vOwAAAAAEBAJ&oi=fnd&dq=%22K.+Berkling%22