Finding two store typings that make the same store valid (lambda-calculus with references) 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:



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?
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.