-1
$\begingroup$

ORIGINAL: I am programming a functional compiler and found out about locally nameless representation (using de brujin indeces for bound variables and names for free variables). I just don't understand what the advantages of locally nameless are?

In uni we made an example language in kotlin with hashmaps as closures. In these hashmaps the variables were stored. In the end we integrated a lexer. I don't understand when locally nameless would even be nessecary, if you wouldnt even be able to get through the lexer when calling something like:

lambda (a) => lambda (a) => a + a

Am I missing something or misunderstanding something?

EDIT: I now understand what it's for and how and when variable capture with named variables happens. I am currently working on an interpreter in kotlin wich takes lambda input and uses locally nameless representation to avoid name capture. I am planning to implement it like this:

  • TEXTINPUT -> Lexer (function definitions with parameters and lambdas)
  • -> Parser (creates the AST of function definitions using de brujin indeces and leaves the parameters as named variables until the function is called)
  • -> Beta reduction(substitute every bound variable and leave the named ones as is)
  • -> function call (Evaluation)

What is your opinion on this sequence?

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ I'm pretty sure any paper on locally nameless is going to talk about the purported advantages of it. What have you looked at so far? $\endgroup$
    – cody
    Jul 19 at 17:36
  • $\begingroup$ Apart from avoiding variable capture, it's supposed to be faster? Or takes less ressources when having a lot of recursion? I just can't imagine a scenario in wich many lambda functions with the same parameter name would occur so that it would matter. Isn't the programmer supposed to pick a different name for most variables anyway? These are my sources so far: youtube.com/watch?v=uhGqJ1A_PRE chargueraud.org/research/2009/ln/main.pdf boarders.github.io/posts/locally-nameless.html $\endgroup$
    – Deonisos
    Jul 19 at 18:32
  • 2
    $\begingroup$ I'm pretty sure it's main advantage is "be less error prone". I'd recommend "I am not a number - I am a free variable" by McBride & McKinna (can be found here). $\endgroup$
    – cody
    Jul 19 at 19:07
  • 3
    $\begingroup$ I'd also have to note that "avoiding variable capture" is quite important in practice. Just look at the introduction to this paper: arxiv.org/abs/2210.04729 $\endgroup$
    – cody
    Jul 19 at 19:10
  • 1
    $\begingroup$ The main use of locally nameless is not in language interpreters, but in interactive theorem proving about programs with bound and free variables. Most foundations of mathematics are not good at making proving facts about capture-avoiding substitution. $\endgroup$
    – Martin Berger
    Jul 19 at 22:27

1 Answer 1

Reset to default
3
$\begingroup$

Locally nameless discipline is important when one has to normalize expressions with free variables. This happens in dependent type theories, where equality of types is tangled up with equality of expressions.

You seem to be suggesting that one could use concrete names (with shadowing). This again does not work at all if you have to perform substitutions of expressions with free variables, as then you must worry about variable capture.

For an implementation of a simply-typed functional language, almost any strategy will work reasonably well. You can use de Bruijn indices, or concrete names (provided that you implement shadowing correctly, which you would anyhow if you didn't do anything strange).

Locally nameless is useless in the implementation of a programming language, because we only ever evaluate closed expressions (programs), so the free variables just never occur, while the bound ones can easily be handled with a runtime environment (implemented in one of several possible ways).

If you ever attempt to implement a dependently type programming language, such as Idris, then you will have to worry about free variables and will be able to appreciate the advantages of locally nameless discipline.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thanks that helps a lot! I understand now in wich cases you would need it. I am already trying to implement it. Now the next problem is when the conversion of free variables to bound variables should happen. Do I convert every scope during parsing? Or do I convert them during evaluation? $\endgroup$
    – Deonisos
    Jul 20 at 17:01
  • $\begingroup$ For a naive approach, have a look at PL Zoo, and the miniml, which uses strings as variable names and compiles a functional language to (simulated) machine code. $\endgroup$
    – Andrej Bauer
    Jul 20 at 22:33
  • $\begingroup$ For locally nameless, look at spartan type theory. Bound variables are converted from strings to de Bruijn indices in the desugaring phase desugar.ml, which happens between parsing and typechecking. There are also routines in TT.ml for converting bound variables to free ones (abstract), and free ones to bound ones (unabstract). $\endgroup$
    – Andrej Bauer
    Jul 20 at 22:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.