# Hindley-Milner system with let expansion

I'm reading these slides that present Hindley-Milner type inference. In the system HM, we have the following let rule:

$$\dfrac{\Gamma \vdash t:S \;\; \Gamma,x:S \vdash t':T }{\Gamma \vdash \text{let} \, x = t \, \text{in} \, t':T}$$

Here $$S$$ is a type scheme, i.e $$S ::= S | \forall a. S$$, which allows polymophism only on let expressions. Then, the following let rule is proposed for a system HM':

$$\dfrac{\Gamma \vdash t:T \;\; \Gamma \vdash [t|x]t':U }{\Gamma \vdash \text{let} \, x = t \, \text{in} \, t':U}$$

so all the occurrences of the binding are replaced and the result needs to be type checked. There is a theorem relating the two approaches:

$$\Gamma \vdash_{HM} t:S \iff \Gamma \vdash_{HM'} t: S$$

and as a consequence the following corollary is established:

Let $$t^*$$ be the result of expanding all let's in $$t$$ according to the rule. $$let \, x = t \, \text{in} \, t' \to [t|x]t'$$. Then, $$\Gamma \vdash_{HM} t:T \implies \Gamma \vdash_{F_1} t^*: T$$. Furthermore, if every let-bound name is used at least once, we also have the reverse $$\Gamma \vdash_{F_1} t^*: T \implies \Gamma \vdash_{HM} t:T$$.

Here $$F_1$$ is the simply-typed lambda-calculus.

I would like to gain some intuition on why this reverse direction holds. How does a let-bound name that is not used affect typing? Any reference is also appreciated.

• Presumably, in $F_1$ a $\lambda$-abstraction is not annotated with a type, i.e., it's written as $\lambda x . t$ (as opposed to $\lambda (x : T) . t$)? Jan 6 '20 at 16:40

I think something somewhat trivial is happening here, that is if the let binding is not used, then you can let bind an ill-typed term, e.g. if:

$$t =\$$let x = (if 3 then 4 else false) in 5

then $$t^* =\$$ 5 which is well-typed in $$\mathrm{HM}$$, even though t is not. If every let-binding is used, though, then this pathology can't happen.

• I'm curious therefore where would find a proof of the statement of the theorem Jan 15 '20 at 9:15
• @Rodrigo If it's not in TAPL, then I'm not sure. It's a pretty good exercise though...
– cody
Jan 15 '20 at 13:04
• I should add that it follows pretty straightforwardly from the lemma that every subterm of a well-typed term is well-typed in STLC, which is a classic lemma to be found in TAPL.
– cody
Jan 15 '20 at 13:05