% -*- Mode: LaTeX -*-

\section{Type Soundness}
\label{sec:soundness}

\subsection{Semantic Consistency}
In order to show the soundness of the typing judgments generated by
the above type system with respect to its evaluation rules, we must
precisely characterize a ``consistent'' semantic relationship between
value-domain entities and their corresponding type-domain entities.
Since values may contain reference locations from the store, we
introduce \cbx{store typings} ($S$) as finite mappings from store
locations to types. We also define that a store typing $S'$
\ibx{extends} another store typing $S$ if
$\fn{Dom}{S}\subseteq\fn{Dom}{S'}$ and $S(l)=S'(l)$ for all
$l\in\fn{Dom}{S}$.  Semantic consistency is now defined below:

\begin{definition}[Semantic Model] \label{defn:consistent} Let
$s$ be a store, $S$ be a store typing, $e$ be an environment, $E$ be a
type environment, $v$ be a value, $\tau$ be a type, and $\sigma$ be a
type scheme. Define the following relations:
\begin{mycases}
\item $S\models{}v:\tau$ --- The value $v$ belongs to the type
$\tau$ under the store typing $S$. The various cases are as follows:
\begin{mysubcases}
\item \label{case:const} 
$S\models{}c:\fn{typeof}{c}$, where \ibx{typeof} is a predefined
relation between predefined constants and their types.
\item \label{case:closure}
$S\models\cval{f,x,a,e}:\tau_{1}\larrow\pi\rarrow\tau_{2}$, if there
exists a type environment $E$ such that $S\models{}e:E$ and
$E\vdash(f\;\tbx{where}\;f(x)=a):\tau_{1}\larrow\pi\rarrow\tau_{2}$.
\item \label{case:ref} 
$S\models{}l:\tau\;\fn{ref}{r}$, if $l\in\fn{Dom}{S}$ and
$S(l)=\tau\;\fn{ref}{r}$.
\item \label{case:nref} 
$S\models{}l:\tau\;\fn{ref}{\epsilon}$, if
$l\in\fn{Dom}{S}$ and there exists a substitution $\varphi$ with
$\fn{Dom}{\varphi}\subseteq\fvar{S(l)}\setminus\dvar{S(l)}$
such that $\varphi(S(l))=\tau\;\fn{ref}{\epsilon}$.
\end{mysubcases}
\item \label{case:scheme} $S\models{}v:\sigma$ --- The value $v$
belongs to the type scheme
$\sigma=\forall\alpha_{1}\ldots\alpha_{n}.\tau$ under the store typing
$S$, if none of $\alpha_{i}$ belong to $\dvar{\tau}$ and if
$S\models{}v:\varphi(\tau)$ for all substitutions $\varphi$ with
$\fn{Dom}{\varphi}\subseteq\{\alpha_{1}\ldots\alpha_{n}\}$.
\item $S\models{}e:E$ --- The values contained in the
environment $e$ belong to the corresponding type schemes in the type
environment $E$ (pointwise) under the store typing $S$, if 
$\fn{Dom}{e}=\fn{Dom}{E}$ and for all
$x\in\fn{Dom}{E}$ we have $S\models{}e(x):E(x)$.
\item \label{case:store} $\models{}s:S$ --- The values contained in the store $s$
belong to the corresponding types in the store typing $S$ (pointwise),
if $\fn{Dom}{s}=\fn{Dom}{S}$ and for all $l\in\fn{Dom}{S}$ we have,
\begin{mysubcases}
\item \label{case:rw} If $S(l)=\tau\;\fn{ref}{r}$ then
$s(l)=v,\/\rw$ and $S\models{}v:\tau$.
\item \label{case:ro} If $S(l)=\tau\;\fn{ref}{\epsilon}$ then
$s(l)=v,\/\ro$ and $S\models{}v:\tau$. 
\end{mysubcases}
\end{mycases}
\end{definition}

The above definition models the type polymorphism and the dynamic
mutability of closed and mutable locations in a consistent manner.
SubCase~\ref{case:nref} allows a closed location (typed using the
null-region $\epsilon$) to be typed polymorphically, while a mutable
location in SubCase~\ref{case:ref} (typed using a region variable $r$)
is allowed to have only a monomorphic type. Similarly, closed
locations in a consistent store are defined to possess the read-only
tag (SubCase~\ref{case:ro}), while mutable locations must have the
read/write tag (SubCase~\ref{case:rw}).

\subsection{Type Soundness and Non-Mutability}

The following proposition establishes the essential correspondence
between the dangerous regions of a type and the mutable locations that
are reachable from a value possessing that type. This allows us to use
dangerous regions as a safe static abstraction for mutable locations.
The proof is done using induction on the {\em depth} of reachability
of a location $l$ in the value $v$.

\begin{proposition}[Region Abstraction] \label{prop:reg-loc}
Let $s$ be a store and $S$ be a store typing such that
$\models{}s:S$. If $S\models{}v:\tau$, $l \in \fn{Reachable}{v,s}$
and $r \in \rvar{S(l)}$, then $r \in \rvar{\tau}$.
That is, the dangerous regions contained in the types of reachable
locations of a value are dangerous in the type of the value. This 
proposition can be extended pointwise to environments.
\end{proposition}

The semantic consistency between the static and the dynamic semantics
can now be stated in the form of the soundness theorem given below.
It is proved using induction on the size of evaluation derivation,
doing a case analysis on $a$ and hence on the last rule used in the
typing derivation.


\begin{theorem}[Type Soundness]
\label{prop:sem-sound} Let $a$ be an expression, $\tau$ be a type, $E$
be a type environment, $e$ be an evaluation environment, $s$ be an
initial store, and $S$ be a store typing such that:
\[E\vdash{}a:\tau\hmm\ibx{and}\hmm{}S\models{}e:E
\hmm\ibx{and}\hmm\models{}s:S\]
If there exists a result $r$ such that $e\vdash{}a/s\Rightarrow{}r$,
then $r\neq\tbx{err}$, instead $r=v/s'$ for some value $v$ and a
resulting store $s'$, and there exists a store typing $S'$ such
that: 
\[S'\;\ibx{extends}\;S\hmm\ibx{and}\hmm{}S'\models{}v:\tau
\hmm\ibx{and}\hmm\models{}s':S'\]
\end{theorem}

The soundness of the \tbx{close} operation relies on the fact that it
only closes \ibx{fresh} and \ibx{non-escaping} locations, \ie,
locations that are neither present in the initial store $s$ nor are
accessible from the environment $e$ or hidden inside the result $v$.
The former is a property of the dynamic rules and the latter is
ensured by the side condition on the static \cbx{close} rule and
\prop{reg-loc}. A proof sketch for this case is provided in the
appendix. The details appear in \cite{Gupta94}.

The soundness theorem immediately leads us to the following corollary
that guarantees that objects with a closed functional type can not be
mutated at run-time. 

\begin{corollary}[Non-Mutability]
Let $a$ be an expression fragment within a type correct program
$p$ such that $E\vdash{}a:\tau$ where $\rvar{\tau}=\phi$ and
$e\vdash{}a/s\Rightarrow{}v/s'$. Then, no location
$l\in\fn{Reachable}{v,s'}$ is mutated during the evaluation of the
rest of the program.
\end{corollary}
\begin{proof}
Using the soundness theorem we know that the evaluation of $p$ (and
hence $a$) does not lead to error and there exists a store typing
$S'\models{}v:\tau$ and $\models{}s':S'$. We claim that for all
locations $l\in\fn{Reachable}{v,s'}$ we must have
$\fn{tag}{s',l}=\ro$.  Otherwise, from \defn{consistent} \case{store}
it follows that there exists a region variable $r_{1}$ such that
$S'(l)=\tau_{1}\;\fn{ref}{r_{1}}$; then using \prop{reg-loc} it
follows that $r_{1}\in\rvar{\tau}$, which contradicts the hypothesis
$\rvar{\tau}=\phi$. 

Now, sound uses of the \cbx{assign} rule in \fig{dynamic} require that
the tag of the location being assigned should be $\rw$.  Furthermore,
there is no rule that converts the tag of a location from $\ro$ to
$\rw$.  Therefore, no assignments are possible on any location
$l\in\fn{Reachable}{v,s'}$ in the rest of the program.
\end{proof}
