4
$\begingroup$

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?

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Lean core type checker has no means to express let constructs. According to the official documentation, all expressions can be translated to this low level representation. How can it be done? $\endgroup$ – user3368561 Apr 2 at 19:14
  • 1
    $\begingroup$ @user3368561 I have no idea about how Lean precisely does that, sorry. $\endgroup$ – chi Apr 2 at 19:58
  • 2
    $\begingroup$ @user3368561 I think they mean eliminating lets by inlining the definition everywhere as in the answer, but you might want to check that this is up to date with the current version. $\endgroup$ – cody Apr 2 at 22:54
  • $\begingroup$ @cody Seems that the type checker (at least one of them) has included an explicit let construct. Maybe the documentation is obsolete in this regard. $\endgroup$ – user3368561 Apr 3 at 6:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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