[Haskell-cafe] Disadvantages of de Bruijn indicies?

[Claus Reinke]

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