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?
$\begingroup$
$\endgroup$
asked May 31 '19 at 13:22
-
$\begingroup$ 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. $\endgroup$ – frabala Jun 1 '19 at 13:20
$\begingroup$
$\endgroup$
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.
