Disadvantages of de Bruijn indicies?
Hi, 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 So I was wondering, are they suitable for use in a compiler? If so, what are their disadvantages/advantages? Is there any particular reason that GHC (as an example) doesn't use them in its Core? I'm trying to decide if I should use them in my compilers data type - and would like some recommendations before I start. Thanks Neil
On Fri, May 11, 2007 at 03:10:42PM +0100, Neil Mitchell wrote:
Hi,
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
So I was wondering, are they suitable for use in a compiler? If so, what are their disadvantages/advantages? Is there any particular reason that GHC (as an example) doesn't use them in its Core?
I'm trying to decide if I should use them in my compilers data type - and would like some recommendations before I start.
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.
There is a brief discussion of the tradeoffs in section 2.5 of the paper "Secrets of the Glasgow Haskell Compiler inliner": http://research.microsoft.com/~simonpj/Papers/inlining/index.htm Stefan
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} }
Neil Mitchell wrote:
Hi,
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
So I was wondering, are they suitable for use in a compiler? If so, what are their disadvantages/advantages? Is there any particular reason that GHC (as an example) doesn't use them in its Core?
I'm trying to decide if I should use them in my compilers data type - and would like some recommendations before I start.
Thanks
The bigest advantage of De Bruijn indices are that: - alpha conversion is not needed and comparison is always modulo renaming. - inlining is very easy I think the largest disadvantage (asside from readability) is that you lose the ability to use a Map as a symbol table for local information (since the names change with each level). Another mayor disadvantage is that it is not immediatly clear how to use De Bruijn numbers with recursive let bindings and case branches, since a single node binds multiple variables. In my toy theorem prover code I use pairs of numbers to solve this, the first is the normal De Bruijn index, the second gives an index into the list of declarations. I believe the Epigram compiler uses De Bruijn numbers for its core language. Have a look at "I am not a number: I am a free variable" by Conor McBride and James McKinna, http://www.e-pig.org/downloads/notanum.pdf Their approach is based on a Scope datatype:
data Scope a = Name :. a Which is used to 'remember' the names of bound variables. This will allow you to largely restore the readability. Another advantage is that code dealing with scoping can be localized.
One final thing I noticed is that a lot of the advantages of De Bruijn numbers disappear if expressions you operate on can have free variables. Say you want to beta reduce (a b), but b contains free variables (in the form of De Bruin indices), now you can no longer just substitute b in a; you have to increment all the indices of the free variables for each scope you enter in a, so these variables are not accedentially captured by that scope. Twan
Neil,
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
So I was wondering, are they suitable for use in a compiler? If so, what are their disadvantages/advantages? Is there any particular reason that GHC (as an example) doesn't use them in its Core?
I'm trying to decide if I should use them in my compilers data type - and would like some recommendations before I start.
De Bruijn indices are used within Epigram, or at least they used to be. Maybe the Epigram people can inform you about their experiences. 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. Cheers, Stefan [1] Conor McBride and James McKinna. Functional pearl: I am not a number—I am a free variable. In Proceedings of the 2004 ACM SIGPLAN Haskell Workshop, Snowbird, Utah, USA, September 22, 2004, pages 1–-9. ACM Press, 2004. http://portal.acm.org/citation.cfm?id=1017472.1017477
Hi
Thanks for all the responses, I'm busy reading through them.
I'm still trying to decide whether I should use them or not. They
complicate things, are less intuitive than names. But on the other
hand, the language I'm working in is untyped and has only letrec.
These things make binding errors easier to occur, and harder to
detect.
Thanks for the helpful throughts,
Neil
On 5/13/07, Stefan Holdermans
Neil,
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
So I was wondering, are they suitable for use in a compiler? If so, what are their disadvantages/advantages? Is there any particular reason that GHC (as an example) doesn't use them in its Core?
I'm trying to decide if I should use them in my compilers data type - and would like some recommendations before I start.
De Bruijn indices are used within Epigram, or at least they used to be. Maybe the Epigram people can inform you about their experiences. 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.
Cheers,
Stefan
[1] Conor McBride and James McKinna. Functional pearl: I am not a number—I am a free variable. In Proceedings of the 2004 ACM SIGPLAN Haskell Workshop, Snowbird, Utah, USA, September 22, 2004, pages 1–-9. ACM Press, 2004. http://portal.acm.org/citation.cfm?id=1017472.1017477
On 13/05/2007, at 12:44, Neil Mitchell wrote:
Hi
Thanks for all the responses, I'm busy reading through them.
I'm still trying to decide whether I should use them or not. They complicate things, are less intuitive than names. But on the other hand, the language I'm working in is untyped and has only letrec. These things make binding errors easier to occur, and harder to detect.
Thanks for the helpful throughts,
Neil
The Calculus of Indexed Names and Named Indices (CINNI) [1] looks really neat: "The Calculus of Indexed Names and Named Indices (CINNI) is a new calculus of explicit substitutions that combines names and indices in a uniform way. It contains the standard named notation used in logics and programming languages as well as de'Bruijn's indexed notation as sublanguages. " Disclaimer: I haven't read the Epigram paper nor Berkling, so I don't know how it compares. And I can't really talk from my own experience, since I have not played myself with CINNI yet. I wish I had a build-a- language assignment, just so that I could put CINNI to work... [1] - http://formal.cs.uiuc.edu/stehr/cinni_eng.html
On Sun, 13 May 2007, Stefan Holdermans
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". -- /NAD
Nils,
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".
Indeed: it is. Cheers, Stefan
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
participants (7)
-
Claus Reinke -
Neil Mitchell -
Nils Anders Danielsson -
Pepe Iborra -
Stefan Holdermans -
Stefan O'Rear -
Twan van Laarhoven