Why 'let' can not be reduce to a lambda application in (extended) Calculus of Constructions

Question

I do not understand the difference highlighted in the chapter 2.5 of the book Theorem Proving in Lean:

Notice that the meaning of the expression let a := t1 in t2 is very similar to the meaning of (λ a, t2) t1, but the two are not the same. In the first expression, you should think of every instance of a in t2 as a syntactic abbreviation for t1. In the second expression, a is a variable, and the expression λ a, t2 has to make sense independently of the value of a. The let construct is a stronger means of abbreviation, and there are expressions of the form let a := t1 in t2 that cannot be expressed as (λ a, t2) t1. As an exercise, try to understand why the definition of foo below type checks, but the definition of bar does not.

def foo := let a := nat  in λ x : a, x + 2
def bar := (λ a, λ x : a, x + 2) nat

What is the explanation behind this?

Answer 1

In an untyped language, those expressions would be equivalent. When working with types, instead, one might have a type while the other one has no type.

Assume that numbers and arithmetic operators all work on $\sf nat$. Then $e_0 = 2+2$ can be typed as $\sf nat$. Now, we can try to perform a $\beta$-expansion, i.e. to "apply $\beta$ backwards", and reach $e_1 = (\lambda x:{\sf nat}.\ x+2)2$.

$$(\lambda x:{\sf nat}.\ x+2)2 \to_\beta 2+2$$

This new expression $e_1$ would still have type $\sf nat$. But we could also go further to $e_2=(\lambda \tau:{\sf Type}.\ (\lambda x:\tau.\ x+2)2){\sf nat}$.

$$(\lambda \tau:{\sf Type}.\ (\lambda x:\tau.\ x+2)2){\sf nat} \to_\beta(\lambda x:{\sf nat}.\ x+2)2 \to_\beta 2+2$$

Now, $e_2$ can not be typed. If it had a type, every subterm of $e_2$ would also be typeable, including $e_2' = (\lambda \tau:{\sf Type}.\ (\lambda x:\tau.\ x+2)2)$, but this subterm can not be typed. The only type we can assign here would be of the form

$$ e_2' : \prod_{\tau:{\sf Type}} (\mbox{something}) $$

in which case this would also be typeable:

$$ e_2' \, {\sf bool} \to_\beta (\lambda x:{\sf bool}.\ x+2)2 $$

The above is nonsense, since $2$ is not a $\sf bool$, so it should not be bound to $x$.

Indeed, we just discovered that types are not preserved under $\beta$-expansion.

A first question arises:

Couldn't we $\beta$-reduce the expression before typing?

Yes, and that's (roughly) what ${\sf let}\ \tau = {\sf nat}\ {\sf in}\ e$ does: it types $e$ knowing that what $\tau$ actually is.

And now one might counter with:

If $\sf let$ works in that way, why don't we use the same technique for lambdas?

We can't do that, since lambdas are not always immediately applied to an argument. The syntax ${\sf let}\ x = t\ {\sf in}\ e$ shows what is the value of $x$, namely $t$. The syntax $(\lambda x. e) t$ also shows the value of $x$ but not all lambdas are used in that way: sometimes we want to use $(\lambda x. e)$ without an argument. Say, we want to pass that to another function $F (\lambda x. e)$, or build a pair of functions $(\lambda x. e, \lambda x. e')$. Here, we don't know what $x$ is. Unlike the $\sf let$ case, here $x$ could even take many values, e.g. if $F = \lambda k. k 0 + k 1$ then $F (\lambda x. e)$ makes $x$ to be $0$ on one call and $1$ in the other call.

So, $\sf let$ is less general than a lambda, and we can have a "special" typing rule for that.