0
$\begingroup$

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?

$\endgroup$
  • $\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 at 13:20
1
$\begingroup$

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.

$\endgroup$

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.