# Find typing derivation of STLC term with reference types

The problem is to find the typing derivation of a term of the call-by-value STLC extended with reference types. The evaluation and typing rules for this language is given in Types and Programming Languages by Pierce on page 166. The term is $$t = (\lambda a:\mathrm{Ref}\mathrm{Bool}. \mathrm{if}\, \mathrm{true}\,\mathrm{then}\, !l_1\, !a\, \mathrm{else}\,0)\,\mathrm{ref}\,\mathrm{true}$$ where $$\mu(l_1)=\lambda x:\mathrm{Int}.x$$ So I need to find $$\Gamma, \Sigma,$$ and $$T$$ so that $$\Gamma\,|\,\Sigma\vdash t:T$$ I know you are supposed to show your work, but my problem is that $$t$$ doesn't seem well-typed... What am I missing?

• If you try to evaluate $t$, this will certainly cause a run-time error. But with an appropriate choice of $\Sigma$, the expression type-checks. Just follow the typing rules from the book. Note that $\mu$ is not involved in these rules. – frabala Jun 1 '19 at 13:20

The expression $$t$$ does not contain any free variables, so one can start typing it with an empty context: $$\emptyset\,|\,\Sigma~\vdash~t : \mathrm{Int}$$, and attempt to build the full derivation tree in a bottom-up way.
The tricky part of the typing derivation is where we try to type-check the subexpression $$(!l_1\,!a)$$. Because $$(!l_1\,!a)$$ lies in the body of a $$\lambda$$-expression which introduces the variable $$a$$ of type $$\text{Ref Bool}$$, at that point the context will be extended with an entry $$(a : \mathrm{Ref~Bool})$$, therefore $$\Gamma=\emptyset,a : \mathrm{Ref~Bool}$$.
$$\dfrac{\dfrac{(a)}{\Gamma\,|\,\Sigma~\vdash~!l_1 : \mathrm{Bool \to Int}}{\text{T-Loc}}~~~~~~~~~~~~~\dfrac{\Gamma\,|\,\Sigma~\vdash~a : \mathrm{Ref~Bool}}{\Gamma\,|\,\Sigma~\vdash~!a : \mathrm{Bool}}{\text{T-Var}}}{\Gamma\,|\,\Sigma~\vdash~!l_1\,!a : \mathrm{Int}}{\text{T-App}}$$
Completing the above sub-derivation by filling in the missing premise in $$(a)$$, shows what $$\Sigma$$ we must choose so that $$t$$ is typable. From the $$\text{T-Loc}$$ rule, clearly $$\Sigma$$ must contain the entry $$(l_1:\mathrm{Bool \to Int})$$.
This contradicts the expectation that $$\Sigma(l_1) = \mathrm{Int \to Int}$$. But this expectation is there only because we know that $$\mu(l_1)$$ is a term of type $$\mathrm{Int \to Int}$$. However, $$\mu$$ plays no role in the typing of an expression. It only plays a role in the evaluation process.
What is violated here is not the typing of $$t$$. Indeed, $$t$$ is straight-forwardly typable by following the typing rules and choosing appropriate $$\Gamma$$ and $$\Sigma$$. What is violated is the typing of $$\mu$$. Following the theory and notation of the book, the judgment $$\Gamma\,|\,\Sigma\vdash\mu$$ does not hold. Because of this, the preservation theorem does not apply and if you try to evaluate $$t$$, a run-time error will occur.