<p>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.</p>
<p>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.</p>
<p>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).</p>
<p>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).</p>
<p>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.</p>

CC BY-SA 4.0
2023-07-20T17:01:43.257Z
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?
Deonisos
CC BY-SA 4.0
2023-07-20T22:33:12.503Z
For a naive approach, have a look at [PL Zoo](https://plzoo.andrej.com), and the [miniml](https://github.com/andrejbauer/plzoo/tree/master/src/miniml), which uses strings as variable names and compiles a functional language to (simulated) machine code.
Andrej Bauer
CC BY-SA 4.0
2023-07-20T22:33:15.893Z
For locally nameless, look at [spartan type theory](https://github.com/andrejbauer/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).
Andrej Bauer
CC BY-SA 4.0
2023-07-20T16:14:20.623Z
2023-07-20T16:14:20.623Z
Andrej Bauer
<p>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?</p>
<p>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:</p>
<pre><code>lambda (a) =&gt; lambda (a) =&gt; a + a
</code></pre>
<p>Am I missing something or misunderstanding something?</p>
<p>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:</p>
<ul>
<li>TEXTINPUT -&gt; Lexer (function definitions with parameters and lambdas)</li>
<li>-&gt; Parser (creates the AST of function definitions using de brujin indeces and leaves the parameters as named variables until the
function is called)</li>
<li>-&gt; Beta reduction(substitute every bound variable and leave the named ones as is)</li>
<li>-&gt; function call (Evaluation)</li>
</ul>
<p>What is your opinion on this sequence?</p>

CC BY-SA 4.0
2023-07-19T17:36:49.567Z
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?
cody
CC BY-SA 4.0
2023-07-19T18:32:04.373Z
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:
https://www.youtube.com/watch?v=uhGqJ1A_PRE
https://chargueraud.org/research/2009/ln/main.pdf 
https://boarders.github.io/posts/locally-nameless.html
Deonisos
CC BY-SA 4.0
2023-07-19T19:07:34.417Z
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](https://web.archive.org/web/20130928162436/https://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf)).
cody
CC BY-SA 4.0
2023-07-19T19:10:14.537Z
I'd also have to note that "avoiding variable capture" is quite important in practice. Just look at the introduction to this paper: https://arxiv.org/abs/2210.04729
cody
CC BY-SA 4.0
2023-07-19T22:27:04.187Z
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.
Martin Berger
CC BY-SA 4.0
2023-07-20T13:51:50.890Z
I'm not even sure people use it when working in theorem provers. A lot of stuff I've seen from that crowd is, "de Bruijn isn't that bad," probably because you _can_ prove your operations correct, and proving magnifies the amount of work involved in a 'complex' scheme like locally nameless. I think where it's useful is complicated syntax-to-syntax transformations where you're _not_ proving them correct. But again, an interpreter is _not_ an example of this, because it's generally not transforming code, and de Bruijn levels are often a perfect match for what it does do.
Dan Doel
CC BY-SA 4.0
2023-07-20T16:08:13.633Z
What is an answer to this question supposed to convey, other than "you're right" or "you're wrong" (opinions)? Is there a specific technical question that we can address?
Andrej Bauer
CC BY-SA 4.0
2023-07-20T17:05:14.753Z
Thanks for all your answers, I am in the process of creating an interpreter in Kotlin for a uni project and the topic I got was locally nameless representation. Since I am not used to functional programming (except for a few lambdas every now and then in javascript), its really hard for me to understand all these formulas. Especially when its explained in Haskell (Wich seems still easier than mathematical formulas). I now understand how and when variable capture with named variables.
Deonisos
CC BY-SA 4.0
2023-07-21T19:11:24.113Z
Please don't use "Original: ... Edit: ....".  Instead, if you have minor clarifications, revise the question so it is self-contained and reads well for someone who encounters it for the first time.  See https://cs.meta.stackexchange.com/q/657/755.  If you have a new question (e.g., the change would invalidate existing answers), please post it separately using the 'Ask Question' button.
D.W.
CC BY-SA 4.0
2023-07-21T19:12:04.817Z
"What is your opinion on this sequence?" is too vague and open-ended to be a good fit here.  We are a question-and-answer site, and we require you to articulate a specific, objectively answerable question.  See our [help/dont-ask].
D.W.
<lambda-calculus><compilers>
Locally nameless representation implementation
Deonisos
# Locally nameless representation implementation

(Asked by: username_0 on 2023-07-19)

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?

**Tags:** lambda-calculus, compilers

> **Comments:**
> **username_1**: 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?  
> **username_0**: 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: https://www.youtube.com/watch?v=uhGqJ1A_PRE https://chargueraud.org/research/2009/ln/main.pdf  https://boarders.github.io/posts/locally-nameless.html  
> **username_1**: 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](https://web.archive.org/web/20130928162436/https://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf)).  
> **username_1**: I'd also have to note that "avoiding variable capture" is quite important in practice. Just look at the introduction to this paper: https://arxiv.org/abs/2210.04729  
> **username_2**: 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.  
> **username_3**: I'm not even sure people use it when working in theorem provers. A lot of stuff I've seen from that crowd is, "de Bruijn isn't that bad," probably because you _can_ prove your operations correct, and proving magnifies the amount of work involved in a 'complex' scheme like locally nameless. I think where it's useful is complicated syntax-to-syntax transformations where you're _not_ proving them correct. But again, an interpreter is _not_ an example of this, because it's generally not transforming code, and de Bruijn levels are often a perfect match for what it does do.  
> **username_4**: What is an answer to this question supposed to convey, other than "you're right" or "you're wrong" (opinions)? Is there a specific technical question that we can address?  
> **username_0**: Thanks for all your answers, I am in the process of creating an interpreter in Kotlin for a uni project and the topic I got was locally nameless representation. Since I am not used to functional programming (except for a few lambdas every now and then in javascript), its really hard for me to understand all these formulas. Especially when its explained in Haskell (Wich seems still easier than mathematical formulas). I now understand how and when variable capture with named variables.  
> **username_5**: Please don't use "Original: ... Edit: ....".  Instead, if you have minor clarifications, revise the question so it is self-contained and reads well for someone who encounters it for the first time.  See https://cs.meta.stackexchange.com/q/657/755.  If you have a new question (e.g., the change would invalidate existing answers), please post it separately using the 'Ask Question' button.  
> **username_5**: "What is your opinion on this sequence?" is too vague and open-ended to be a good fit here.  We are a question-and-answer site, and we require you to articulate a specific, objectively answerable question.  See our [help/dont-ask].  

---

## 1 answers

### Answer by username_4 on 2023-07-20. Score: 4

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.

> **Comments:**
> **username_0**: 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?  
> **username_4**: For a naive approach, have a look at [PL Zoo](https://plzoo.andrej.com), and the [miniml](https://github.com/andrejbauer/plzoo/tree/master/src/miniml), which uses strings as variable names and compiles a functional language to (simulated) machine code.  
> **username_4**: For locally nameless, look at [spartan type theory](https://github.com/andrejbauer/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).  

---

