Lambda Calculus Identity Function

Question

Dr. Benjamin Pierce's "Types and Programming Languages" mentions the identify function on page 55:

$id = \lambda x.x$;

I understand the identity function from usage in Haskell:

id' :: a -> a
id' x = x

It accepts a single argument and returns it.

But, what does $\lambda x.x$ mean in the above id function's right-hand side? Please break down each component of the function.

Example, in the Haskell id', id' is the function's name. a is the input type and a is the output type. The x represents the input argument value and, consequently, the output value.

Answer 1

Let's try to break down the syntax of λx. x into pieces:

• λ means that you are dealing with an abstraction (it is a fancy word for function in programming sense). It doesn't mean anything and it is there just for parsing purposes. See here if you are curious why this particular letter was chosen.
• the first x occurrence -- it is called binding occurrence -- is a formal parameter name, just like Haskell's version first x after id.
• . is a separator between the formal parameter name and the abstraction's body. It's there for parsing only.
• the second occurrence of x constitutes the abstraction's body, which is like a Haskell function's body.

A couple comments:

• $id = \lambda x. x$ is not a piece of $\lambda$-calculus syntax, because it doesn't have =. So if you see something like id y you need to do "macro-expansion" of id to get a valid $\lambda$-term.
• λx. x is usually not a valid $\lambda$-term as well. It is syntactic sugar for (λx. x). It is customary to get rid of the top-level parentheses and to drop some more parentheses while introducing the rules that prevent ambiguity.