[Haskell-cafe] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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}
}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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 <[EMAIL PROTECTED]> wrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
On Sun, 13 May 2007, Stefan Holdermans <[EMAIL PROTECTED]> wrote: > 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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=vOwAEBAJ&oi=fnd&dq=%22K.+Berkling%22 ___
