11.5 Let Bindings

---

11.5 Let Bindings

When writing a complex expression, it is often useful-both for avoiding repetition and for increasing readability-to give names to some of its subexpressions. Most languages provide one or more ways of doing this. In ML, for example, we write let x=t₁ in t₂ to mean "evaluate the expression t₁ and bind the name x to the resulting value while evaluating t₂.

Our let-binder (summarized in Figure 11-4) follows ML's in choosing a call-by-value evaluation order, where the let-bound term must be fully evaluated before evaluation of the let-body can begin. The typing rule T-LET tells us that the type of a let can be calculated by calculating the type of the let-bound term, extending the context with a binding with this type, and in this enriched context calculating the type of the body, which is then the type of the whole let expression.

Figure 11-4: Let Binding

11.5.1 Exercise [Recommended, ⋆⋆⋆]

The letexercise typechecker (available at the book's web site) is an incomplete implementation of let expressions: basic parsing and printing functions are provided, but the clauses for TmLet are missing from the eval1 and typeof functions (in their place, you'll find dummy clauses that match everything and crash the program with an assertion failure). Finish it.

Can let also be defined as a derived form? Yes, as Landin showed; but the details are slightly more subtle than what we did for sequencing and ascription. Naively, it is clear that we can use a combination of abstraction and application to achieve the effect of a let-binding:

But notice that the right-hand side of this abbreviation includes the type annotation T₁, which does not appear on the left-hand side. That is, if we imagine derived forms as being desugared during the parsing phase of some compiler, then we need to ask how the parser is supposed to know that it should generate T₁ as the type annotation on the λ in the desugared internal-language term.

The answer, of course, is that this information comes from the typechecker! We discover the needed type annotation simply by calculating the type of t₁. More formally, what this tells us is that the let constructor is a slightly different sort of derived form than the ones we have seen up till now: we should regard it not as a desugaring transformation on terms, but as a transformation on typing derivations (or, if you prefer, on terms decorated by the typechecker with the results of its analysis) that maps a derivation involving let

to one using abstraction and application:

Thus, let is "a little less derived" than the other derived forms we have seen: we can derive its evaluation behavior by desugaring it, but its typing behavior must be built into the internal language.

In Chapter 22 we will see another reason not to treat let as a derived form: in languages with Hindley-Milner (i.e., unification-based) polymorphism, the let construct is treated specially by the typechecker, which uses it for generalizing polymorphic definitions to obtain typings that cannot be emulated using ordinary λ-abstraction and application.

11.5.2 Exercise [⋆⋆]

Another way of defining let as a derived form might be to desugar it by "executing" it immediately-i.e., to regard let x=t₁ in t₂ as an abbreviation for the substituted body [x ↦ t₁]t₂. Is this a good idea?

---