[Haskell-cafe] Disadvantages of de Bruijn indicies?

[Claus Reinke]

>> 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=.html

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}
}