% -*- Mode: LaTeX -*-

\section{Static Semantics}
\label{sec:static-semantics}
Now we will briefly describe Xavier Leroy's closure typing system
\cite{Leroy92} and our extensions to it. A type $\tau$ in our system
is defined by:
\[\cbx{types:}\hmmmm \tau ::= t \; | \; \iota \; | \;
\tau_{1}\larrow\pi\rarrow\tau_{2} \; | \; \tau \; \fn{ref}{r} \; | \;
\tau \; \fn{ref}{\epsilon} \] 
where $t$ corresponds to an ordinary type variable and $\iota$
corresponds to a base type. Type schemes ($\sigma =
\forall\alpha_{1}\ldots\alpha_{n}.\tau$) are quantified types.

Functions in Leroy's system are decorated with a set of {\em closure
types} (denoted by $\pi = \sigma_1,\sigma_2,\ldots,u$), which
corresponds to the type schemes of the free identifiers of a function.
The closure extension variable $(u)$ allows us to extend the set of
closure types in a meaningful manner during type unification. These
closure types are useful in keeping track of the mutable objects
hidden inside a dynamic function closure.

We extend the closure typing system by parameterizing type
constructors with {\em regions}. A region variable parameter $(r)$ on
a reference type constructor serves two purposes.  It identifies the
reference type as being mutable and it also serves as a static
abstraction for all the mutable locations that have that type.
Non-mutable references are identified by a null region parameter
$(\epsilon)$ which shows that they have been closed.  Note that
\fn{ref}{r} and \fn{ref}{\epsilon} are considered to be distinct type
constructors for the purpose of type unification; they have a similar
form only for syntactic uniformity.

For any type object $T$, where $T$ may be a type, a closure type, a
region, or a type scheme, we can define its \cbx{free variables}
$\fvar{T}$ as the set of all type, region, and closure extension
variables contained in $T$. We also define the \cbx{dangerous
variables} $\dvar{T}$ as follows:
\[\begin{array}{rcl@{\hmmm}rcl}
\dvar{t}        & = & \phi              &
\dvar{u}        & = & \phi              \\
\dvar{\iota}    & = & \phi              &
\dvar{\sigma,\pi} & = & \dvar{\sigma}\cup\dvar{\pi} \\ 
\dvar{\tau_{1}\larrow\pi\rarrow\tau_{2}} & = & \dvar{\pi} &
\dvar{r}        & = & \phi              \\
\dvar{\tau\;\fn{ref}{r}} & = & \fvar{\tau\;\fn{ref}{r}} &
\dvar{\forall\alpha_{1}\ldots\alpha_{n}.\;\tau} & = &
\dvar{\tau}\setminus\{\alpha_{1}\ldots\alpha_{n}\} \\
\dvar{\tau\;\fn{ref}{\epsilon}} & = & \dvar{\tau} & 
\dvar{\epsilon} & = & \phi             
\end{array}
\]
Finally, the \cbx{dangerous region variables} $\rvar{T}$ are the
region variables in $\dvar{T}$.

\cbx{type substitutions} ($\varphi$) over this type algebra are finite
mappings from regular type variables to types, from closure extension
variables to closure types, and from region variables to other region
variables.  We do not allow substituting region variables with the
null region ($\epsilon$) because that would convert a mutable
reference type into a non-mutable reference type. This operation
should only be performed when it is determined to be safe and is
explicitly done using the \tbx{close} construct.  Type substitutions
extend naturally over types, closure types, and type schemes, being
applied to their free variables in each case.  The \ibx{instantiation}
of a type scheme $\sigma=\forall\alpha_{1}\ldots\alpha_{n}.\tau_{0}$
to a type $\tau$, written as $\sigma\geq\tau$, is defined if there
exists a type substitution $\varphi$ with
$\fn{Dom}{\varphi}\subseteq\{\alpha_{1}\ldots\alpha_{n}\}$ such that
$\tau=\varphi(\tau_{0})$.

The basic idea of our type system is to use the type of a composite
object as a clue to the reachable mutable reference locations
contained within it. Dangerous variables provide this clue directly
from the overall type of an object. Intuitively, dangerous \ibx{type}
variables model the polymorphic values stored in mutable
data-structures and the dangerous \ibx{region} variables model the
locations of those mutable data-structures.

\subsection{Typing Rules}
\begin{myfig}{fig:static}{The Static Semantics of the Mini-Language.}
\begin{center}
\begin{tabular}{l@{\hmmmm}c}
\cbx{const:} & 
\inference{\stmt{\fn{typeof}{c}\geq\tau}}%
          {\stmt{E\vdash{}c:\tau}} \\ \\
\cbx{ident:} & 
\inference{\stmt{x\in\fn{Dom}{E}\hmm E(x)\geq\tau}}%
          {\stmt{E\vdash{}x:\tau}} \\ \\
\cbx{abs:} &
\inference{\stmt{\{y_{1}\ldots{}y_{n}\}=\fvar{f\;\tbx{where}\;f(x)=a}} \\
           \stmt{E+\{f\mapsto\tau_{1}\larrow{}E(y_{1}),\ldots,E(y_{n}),
                 \pi\rarrow\tau_{2},x\mapsto\tau_{1}\}\vdash{}a:\tau_{2}}}%
          {\stmt{E\vdash(f\;\tbx{where}\;f(x)=a):\tau_{1}\larrow{}E(y_{1}),
           \ldots,E(y_{n}),\pi\rarrow\tau_{2}}} \\ \\
\cbx{app:} &
\inference{\stmt{E\vdash{}a_{1}:\tau_{1}\larrow\pi\rarrow\tau_{2}}\hmm
           \stmt{E\vdash{}a_{2}:\tau_{1}}}%
          {\stmt{E\vdash{}a_{1}\;a_{2}:\tau_{2}}} \\ \\
\cbx{let:} &
\inference{\stmt{E\vdash{}a_{1}:\tau_{1}}\hmm
           \stmt{E+\{x\mapsto\fn{Gen}{E,\tau_{1}}\}\vdash{}a_{2}:\tau_{2}}}%
          {\stmt{E\vdash(\tbx{let}\;x=a_{1}\;\tbx{in}\;a_{2}):\tau_{2}}} \\ \\
\cbx{close:} &
\inference{\stmt{E\vdash{}a:\tau\;\fn{ref}{r}} \hmm
           \stmt{r\not\in(\fvar{E}\cup\fvar{\tau})}}%
          {\stmt{E\vdash(\tbx{close}\;a):\tau\;\fn{ref}{\epsilon}}}
\end{tabular}
\end{center}
\end{myfig}

\fig{static} shows the axioms and inference rules for
establishing \cbx{elaboration judgments} of the form
$E\vdash{}a:\tau$, where $E$ is a type environment that maps
identifiers to type schemes. The \cbx{const} rule establishes the type
of a constant according to a predefined relation \ibx{typeof} that
provides the type scheme associated with it.  Most constants and
operators have the obvious type schemes. We only show the predefined
type schemes of the three reference operators below:
\[\begin{array}{rcl}
\fn{typeof}{\tbx{ref}} & = &
\forall{}t,u,r.\;t\larrow{}u\rarrow{}t\;\fn{ref}{r} \\
\fn{typeof}{\tbx{!}_{\sibx{mutable}}} & = &
\forall{}t,u,r.\;t\;\fn{ref}{r}\larrow{}u\rarrow{}t \\
\fn{typeof}{\tbx{!}_{\sibx{non-mutable}}} & = &
\forall{}t,u.\;t\;\fn{ref}{\epsilon}\larrow{}u\rarrow{}t \\
\fn{typeof}{\tbx{:=}} & = &
\forall{}t,u,r.\;(t\;\fn{ref}{r},t)\larrow{}u\rarrow\ibx{unit} 
\end{array}\]

The \cbx{const}, \cbx{ident}, \cbx{app}, and \cbx{let} rules are
standard Hindley/Milner typing rules \cite{Milner78}.  The
\ibx{generalization} operation in the \cbx{let} rule excludes the
dangerous variables $\dvar{\tau}$ from being generalized:
\[ \fn{Gen}{E,\tau} = \forall\alpha_{1}\ldots\alpha_{n}.\tau
\hm\bx{where}\hm \{\alpha_{1}\ldots\alpha_{n}\} =
\fvar{\tau}\setminus\dvar{\tau}\setminus\fvar{E}\] 
This ensures that the type variables corresponding to mutable objects
are not generalized, making our type-generalization sound.

The \cbx{abs} rule shows how closure types are created in this system.
The type schemes of all the free identifiers of the function are
stored in its closure type.  This helps to expose the mutable
locations hidden inside the closure environment of a function so that
closing such data-structures may be caught as a compile-time
close-error (Example~\ref{ex-escape}).

Finally, the \cbx{close} rule converts a mutable reference type into a
non-mutable reference type by \ibx{erasing} its region variable $r$
and replacing it with the null region ($\epsilon$). By checking that
$r$ does not occur free in the type environment $E$ or in the exported
type $\tau$, we ensure that the corresponding reference location $l$
being closed is not escaping from the current scope. Informally,
$r\not\in\fvar{E}$ implies that $l$ is not reachable from the value
environment ($e$) and $r\not\in\fvar{\tau}$ implies that $l$ is not
recursively reachable from the value stored in the location $l$. Thus,
no write handle to the location $l$ is escaping and it can be safely
closed. A compile-time close-error is flagged if this check fails.

As an aside, we note that a type inference algorithm can be designed
for this type system along the lines of \cite{Leroy92}. We do not
discuss that here, the reader is referred to \cite{Leroy92} for
details.
