i can't seem to find much info on the following question:

how (if at all) is the fixing of names to values (by binding or assignment) possible in a purely functional system like the lambda calculus?

i've seen examples of this being done in haskell, lisp etc. by using the 'let' or '=' operators. to me it always reads like "kicking the can down the road" to a place where, out of sight, something non-functional is happening to make the language more practical/easy to use.

i am fairly new to the world of functional programming, so i may well be overlooking something obvious. if anyone here can point me to some material on the topic or give a basic explanation, i'd be very grateful :)


2 Answers 2


The lambda calculus has names for the parameter (bound variable) to a lambda abstraction. That is the only mechanism or introducing names. Apart from that, there are no names in the lambda calculus. Notice that there is no assignment within the lambda calculus.

There is nothing non-functional being hidden here.

If you are new to functional programming, I would not recommend starting with the lambda calculus. It is elegant from a theoretical perspective, but hard to develop intuition for from the perspective of a practical programmer.


I suspect you're imagining $\text{let } x = E \text{ in } E'$ as describing a sequence of steps: take the thing described by $E$ and put it in the box labeled $x$, then proceed to the thing labeled $E'$. It will seem less imperative if you take a less imperative view of it. Real functional languages are of necessity compiled/interpreted on hardware that has a non-functional design, so it's likely that at some point a machine instruction will execute that puts a value representing $E$ into a register or RAM location representing $x$, and then later instructions will be related to $E'$, but that's not really the fault of the high-level language, and you don't have to conceptualize the high-level language in terms of those low-level details.

A traditional view is that $\text{let } x = E \text{ in } E'$ means $(λx.E')\,E$. In LISP-family languages, it may literally desugar to that. $(λx.E')\,E$ is then ("beta-")equivalent to $E'[E/x]$, meaning $E'$ with $E$ substituted for $x$ wherever $x$ appears. This is a true mathematical equivalence: you can just as well start with $E'[E/x]$ and turn it into $(λx.E')\,E$. The desugaring of $\text{letrec}$ is more complicated and requires a Y combinator or something like it.

What I wrote in the last paragraph only applies to a pure functional language in the LISP family, and I don't know if any such exists. In real LISPs, the desugaring of $\text{letrec}$ uses setq/set!, and beta-equivalence doesn't work because of side effects. Haskell is purely functional, but $\text{let}$ and $λ$ bindings aren't equivalent in Haskell or other ML-family languages because there are special typing rules for $\text{let}$.

My favorite way of understanding $\text{let}$ and $\text{letrec}$ is that they generalize expression trees to rooted expression graphs. Without them, every expression is a tree (its abstract syntax tree). With $\text{let}$, you can also describe dags. For example, $\text{let } x = E \text{ in } x*(x+1)$ means this dag, with all edges pointing downward:

/ \
|  +
| / \
 E   1

The symbol $x$ is needed by the $\text{let}$ notation, but it doesn't appear in the dag, where $E$ is not assigned or bound to anything. Roughly speaking, in this view, $\text{let } x = E \text{ in } E'$ means $E'[E/x]$, except that if $x$ appears more than once, you imagine that $E$ is shared rather than textually duplicated. Adding $\text{letrec}$, you can also represent graphs with cycles. No Y combinator is involved: all of the edges point to their referents directly.


Your Answer

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

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