Problem 13.5.2 of Pierce's TAPL's book (page 167) asks:

Can you find a context $\Gamma$, a store $\mu$ and two different store typings $\Sigma_1,\Sigma_2$ such that both $\Gamma | \Sigma_1 \vdash \mu$ and $\Gamma | \Sigma_2 \vdash \mu$?

I'm not getting the proposed solution:

enter image description here

But how can this be the case? I mean should not $l$ be of a reference type $Ref(T_1)? $ How can it be of function type?

  • $\begingroup$ What is $!$ in that context? $\endgroup$
    – siracusa
    Nov 7, 2019 at 23:41
  • $\begingroup$ @siracusa It's the dereference operator: !l is the value stored in the reference l. $\endgroup$ Nov 8, 2019 at 7:11

1 Answer 1


The store $\mu$ indicates the type of what is stored in the reference. If $\Sigma(\ell) = T$ then the expression $!\ell$ has the type $T$, and the expression $\ell$ has the type $\mathsf{Ref}(T)$.

If all you need is for $\lambda x:\mathsf{Unit}. (!\ell)(x)$ to be well-typed, then $\ell$ must be a reference to a function whose argument type is $\mathsf{Unit}$, with no constraint on the return type.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.