de Bruijn indicies look quite nice, and seem to eliminate a lot of complexity when dealing with free variables: http://en.wikipedia.org/wiki/De_Bruijn_index
the complexity is not really eliminated, but made precise and mechanised, which is helpful for tools, less helpful for humans.
From what I've heard, the main disadvantage is that they make Core nigh-impossible to read - which is important because you will spend much much more time debugging your compiler than writing it.
if readability is an issue, you might consider Berkling's "symmetric complement to the lambda-calculus" [1] instead. in brief, he added a protection key to the calculus (to complement the lambda binder), so that in '\x->\x->x /x', the first 'x' would be bound to the inner lambda, the second, protected '/x' would be bound to the outer lambda. that gets the best of both worlds, in fact, both ordinary and de Bruijn's lambda calculus are subsets of Berkling's (avoid protection keys, or use a single variable name only). since haskell does not have protection keys in the source language, you'd only get them through compiler manipulations, whereas the unmanipulated parts of the source would be free of them. and in all cases, you'd still have the names at hand. you'd probably have a hard time getting your hands on the original techreport (from the pre-online, pre-reorganisation times of the German "Gesellschaft fuer Mathematik und Datenverarbeitung";-) there were later publications on the topic, such as items 5 and 6 in this bibliography: http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/b/Berkling:Klaus_J... as with all arithmetic, typesetting is a great way of obscuring the important details while trying to make them more obvious. my own attempt can be found in section 2.2 of my old phd thesis: http://www.cs.kent.ac.uk/people/staff/cr3/publications/phd.html for a more recent, executable attempt, you could try darcs get http://www.cs.kent.ac.uk/~cr3/fathom and have a look at 'fathom.txt', and 'Lambda.hs' ;-) hth, claus [1] @techreport{Berkling76, author = {Berkling, K.J.}, title = {{A Symmetric Complement to the Lambda Calculus}}, institution = GMD, note = {ISF-76-7}, month = {September}, year = 1976, abstract = {"The calculi of Lambda-conversion" introduced by A.Church are complemented by a new operator lambda-bar, which is in some sense the inverse to the lambda-operator. The main advantage of the complemented system is that variables do not have to be renamed. Conversely, any renaming of variables in a formula is possible. Variables may, however, appear with varied numbers of lambda-bars in front of them. Implementations of the lambda calculus representation with the symmetric complement are greatly facilitated. In particular, a renaming of all variables in a formula to the same one is possible. Variables are then distinguished only by the number of preceding lambda-bars. Finally, we give a four symbol representation of the lambda calculus based on the above mentioned freedom in renaming. }, topics = {FP - Lambda Calculi} }