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

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

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.