1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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$)? $\endgroup$ – Andrej Bauer Jan 6 at 16:40
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I'm curious therefore where would find a proof of the statement of the theorem $\endgroup$ – Rodrigo Jan 15 at 9:15
  • $\begingroup$ @Rodrigo If it's not in TAPL, then I'm not sure. It's a pretty good exercise though... $\endgroup$ – cody Jan 15 at 13:04
  • $\begingroup$ 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. $\endgroup$ – cody Jan 15 at 13:05

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.