% File: locality3.tex
% Status: Last modification by Florian 28-DEC-1990
%
\section{Typing Objects with Locality}
\label{sec:types}

In a conventional type system, a type represents the structure of a
value and typechecking is the process of checking the consistency  of
operations with respect to the structures of the values involved. Our
goal is to extend such a conventional type system to include repository
information so that a type also captures the dependency of a value on
repositories. The type system can thereby also check the consistency of
reference creation and manipulation with respect to reachability
constraints among repositories. In this section we will develop such a
type system.

\subsection{Types and Localities}
An expression, in general, contains references through which it
depends on a set of repositories.  We call this dependency the {\em
locality\/} of an expression.  Formally, a locality $\pi$ is a set of
repositories. The first step in defining the type system is to enrich
the language of types to include locality information.  Since types in
a static type system must be static entities, i.e.\ they must be
denotable at compile-time, we assume that the set of repositories and
their reachability sets are known at compile-time. This is certainly a
restriction as it prohibits a dynamic reconfiguration of
repositories.  The relaxation of this restriction is a topic of future
interest. We will take this point up later in
section~\ref{sec:conclusions}.

It turns out that the only type constructors that require an explicit
locality specification are:
\begin{program}$\tau_1\funtype{\pi}\tau_2$\ \ \ \ \=\kill
ref($\pi$,$\tau$)\>{\it the reference type constructor, and}\\
$\tau_1\funtype{\pi}\tau_2$\>{\it the function type constructor.}
\end{program}%
A value of a reference type {\tt ref($\pi$,$\tau$)} is a reference in
one of the repositories of $\pi$. $\tau$ specifies the type of the
referenced value. Note that the repository information is ambiguous
unless $\pi$ is a singleton set. As we shall see later, this ambiguity
is viatal in achieving a smooth mixture of lists (or more general
collection types) and references.

The locality tag $\pi$ in $\tau_1\funtype{\pi}\tau_2$ means that a
function may possibly manipulate references in $\pi$. To see the need
of this explicit locality tag, consider the following functions.
\begin{program}
f $=$ $\lambda$x:ref(\{R\},int).$\lambda$y:int.(!x) + y;\\
g $=$ f(\kwd{new}(R,2))
\end{program}%
{\tt F} is a function that takes a reference {\tt x} to an integer in a
repository {\tt R} and returns a function that increments its argument
{\tt y} by the dereferenced value {\tt !x}.  The expression {\tt g},
therefore, is a function which takes an integer and returns an
integer.  In a conventional type system it is given the type {\tt
int$\func$ int}.  Although neither its domain type nor its range type
have a connection to any repository, {\tt g} nevertheless  depends on
the repository {\tt R} through the static environment where the
variable {\tt x} is bound to a reference in $R$.  To completely
capture the localities of values involving functions, we must record
such dependencies within the type of an expression. Therefore, {\tt g}
has type {\tt int}$\funtype{\{R\}}${\tt int} in our type system.

\label{func-environment}
The meaning of the  extra locality tag $\pi$ in function types can
also be illustrated by looking at standard implementations of
functional languages,  where a run-time value of a function type is a
function closure containing an environment and it is this environment
that induces the dependency of the value to repositories. 

With these refinements, the set of types is given by the following
abstract syntax:
\begin{program}
$\tau$ $::=$ $b$\vbar unit\vbar$\tau\funtype{\pi}\tau$\vbar%
\record{$l$:$\tau$,$\ldots$,$l$:$\tau$}\vbar% 
\bdt{$\tau$}\vbar ref($\pi$,$\tau$)
\end{program}%
{\tt unit} is the trivial type whose only value is {\tt Void}. $b$
ranges over base types.  {\tt
\record{$l$:$\sigma$,$\ldots$,$l$:$\sigma$}} stands for record types
and {\tt \bdt{$\tau$}} for set types.

Types in our system not only represent the structure of values but they
also represent their locality.  The locality $\locality(\tau)$
represented by the type $\tau$ is defined inductively as follows:
\begin{eqnarray*}
\locality(b) &=& \emptyset\\
\locality(\code{unit}) &=& \emptyset\\
\locality(\tau_1\funtype{\pi}\tau_2) &=& \pi\\
\locality(\code{\record{$l_1$:$\tau_1$,$\ldots$,$l_n$:$\tau_n$}}) &=&
   \bigcup\{\locality(\tau_1)|1\le i\le n\}\\
\locality(\code{\bdt{$\tau$}}) &=& \locality(\tau)\\
\locality(\code{ref($\pi$,$\tau$)}) &=& \pi
\end{eqnarray*}
Note that the domain type and the range type of a function type do not
induce any dependency. The rule for reference types reflects our
decision that the reachability constraint specified by the map $\mu$
is {\em shallow}. The locality of the type {\tt ref($\pi$,$\tau$)} is
always $\pi$ irrespective of the locality of $\tau$. If a {\em deep\/}
restriction were preferred, then the required rule would be:
\begin{eqnarray*}
\locality(\code{ref($\pi$,$\tau$)}) &=&\pi\cup\locality(\tau)
\end{eqnarray*}

\subsection{Typing Rules}
We are now in a position to define a proof system for {\em typing
judgements\/} in such a way that for any well-typed program (closed
expression) $P$, a static typing judgement $P:\tau$ implies the
following three desirable properties of the (dynamic) evaluation of
$P$.
\begin{enumerate}
\item The structure of the value produced by $P$ conforms to the
structural part of $\tau$;
\item The locality of the value produced by $P$ conforms to
$\locality(\tau)$;
\item The reference environment (the object store) does not violate
the predefined reachability constraint imposed by $\mu$.
\end{enumerate}

Since expressions in general contain free variables, a typing judgement
is defined with respect to a {\em type assignment\/} $\ass$ which is a
function from a finite subset of variables to types.  We write
$\ass\{x\mapsto \tau\}$ for the function $\ass'$ such that $dom(\ass')
= dom(\ass)\cup \{x\}$, $\ass'(x) = \tau$, and $\ass'(y) = \ass(y)$ if
$y\not = x$.  We write $\typing{\ass}{M}{\tau}$ if expression $M$ has
type $\tau$ under type assignment $\ass$. In the rest of this
section, we analyze each of the expression constructors and define 
their typing rules.

\begin{figure}[ht]
{\small\tt
\axiom{{\sc (const)}}
        {$\typing{\ass}{(c:\tau)}{\tau}$}\rvsep\\
\axiomc{{\sc (var)}}
        {$\typing{\ass}{x}{\tau}$}
        {if $x\in dom(\ass), \ass(x) = \tau$}\rvsep\\
\ruletwo{{\sc (app)}}
        {$\typing{\ass}{M_1}{\tau_1\funtype{\pi}\tau_2}$}
        {$\typing{\ass}{M_2}{\tau_1}$}
        {$\typing{\ass}{\code{$M_1$($M_2$)}}{\tau_2}$}\rvsep\\
\ruleone{{\sc (record)}}
        {$\typing{\ass}{M_i}{\tau_i}$\ $(1\le i\le n)$}
        {$\typing{\ass}{\code{\record{$l_1$=$M_1$,$\ldots$,$l_n$=$M_n$}}}
           {\code{\record{$l_1$:$\tau_1$,$\ldots$,$l_n$:$\tau_n$}}}$}\rvsep\\
\ruleonec{{\sc (dot)}}
        {$\typing{\ass}{M}{\tau_1}$}
        {$\typing{\ass}{M.l}{\tau_2}$}
        {{\rm if $\tau_1$ is a record type with $l:\tau_2$}}\rvsep\\
\ruletwoc{{\sc (modify)}}
        {$\typing{\ass}{M_1}{\tau_1}$}
        {$\typing{\ass}{M_2}{\tau_2}$}
        {$\typing{\ass}{\code{\kwd{modify}($M_1$,$l$,$M_2$)}}{\tau_1}$}
        {{\rm if $\tau_1$ is a record type with $l:\tau_2$}}\rvsep\\
\axiom{{\sc (empty)}}
        {$\typing{\ass}{\code{(nil:\bdt{$\tau$})}}{\code{\bdt{$\tau$}}}$}\rvsep\\
\ruleone{{\sc (head)}}
        {$\typing{\ass}{M}{\code{\bdt{$\tau$}}}$}
        {$\typing{\ass}{\code{\kwd{head}($M$)}}{\tau}$}\rvsep\\
\ruleone{{\sc (tail)}}
        {$\typing{\ass}{M}{\code{\bdt{$\tau$}}}$}
        {$\typing{\ass}{\code{\kwd{tail}($M$)}}{\code{\bdt{$\tau$}}}$}\rvsep\\ 
\ruleone{{\sc (deref)}}
        {$\typing{\ass}{M_1}{\code{ref($\pi$,$\tau$)}}$}
        {$\typing{\ass}{\code{\deref{$M_1$}}}{\tau}$}\rvsep\
}
\caption{The remaining typing rules}
\label{fig:typing}
\end{figure}

We start with references. For reference creation {\tt
\kwd{new}($R$,$M$)}, we must ensure that the locality of $M$ satisfies
the reachability constraint $\mu(R)$. This is expressed in our
type system as $\locality(\tau)\subseteq \mu(R)$ where $\tau$ is the
type of $M$. The desired typing rule for reference creation is then
given as:
\rvsep\\
{\tt
\ruleone{{\sc (new)}}
	{$\typing{\ass}{M}{\tau}$}
	{$\typing{\ass}{\code{\kwd{new}($R$,$M:\tau$)}}
          {\code{ref($\{R\}$,$\tau$)}}$}
        {\mbox{\ \ \ if }$\locality(\tau)\subseteq \mu(R)$}\rvsep\\
}
For example, in the previous section, we considered the two
repositories {\tt Permanent} and {\tt Temporary} with the associated
reachability sets $\mu(\code{Permanent}) = \emptyset$ and
$\mu(\code{Temporary}) = \{\code{Permanent}\}$ and created references
named {\tt helen}, {\tt john}, {\tt joe} and {\tt susan}. All of them
are legal and the following typings are derivable:
\begin{program}
helen: ref(\{Permanent\}, [Name:string, Age:int])\\
john: ref(\{Temporary\}, [Name:string, Age:int])\\
joe: ref(\=\{Permanent\}, [Name:string, Age:int,\\
     \>Boss:ref(\{Permanent\}, [Name:string, Age:int])])\\
susan: ref(\=\{Temporary\}, [Name:string, Age:int,\\
     \>Boss:ref(\{Permanent\}, [Name:string, Age:int])])
\end{program}%
The reachability constraint among repositories is enforced by the side
condition $\locality(\tau)\subseteq \mu(R)$ of the typing rule {\sc
(new)}. In the case of {\tt susan}, for example, the condition is
\begin{program}
$\locality($[\=Name:string, Age:int,\\
   \>Boss:ref(\{Permanent\}, [Name:string, Age:int])]$)$\\
$\subseteq$ $\mu({\tt Temporary})$ $=$ $\{$Permanent$\}$
\end{program}%
which is indeed true. The rule for dereferencing is standard (see
Fig.~\ref{fig:typing}). We will consider the rule for assignment after
considering the interaction between references and lists.

The locality of each of the above reference types is a singleton set
representing the exact repository of the reference. More flexible or
{\em ambiguous\/} reference types become necessary  when we want to
achieve a smooth interaction between references and lists. In order to
make locality information as transparent as possible to those users who
do not make any use of it, we would like to allow lists which contain
references of different localities as long as their structure is the
same. This conflicts with the (strictly homogeneous) list type
constructor.  In order to typecheck statically the elimination
operation \kwd{head}, lists must be homogeneous while objects with
different localities have different types. We reconcile this conflict
by {\em weakening\/} the locality information of the element type of a
list type. Remember that a value of the type {\tt ref($\pi$,$\tau$)}
is a reference in {\em one of\/} the repositories in $\pi$. This
ambiguity allows us to assign a type to a list containing elements
with different localities. For example, the list {\tt \{helen, john\}}
is given the type {\tt \bdt{ref(\{Permanent, Temporary\},[Name:string,
Age:int])}}. A value of this type is a list whose elements are
references either in {\tt Permanent} or {\tt Temporary}. This
idea is generalized to arbitrary complex types by exploiting the
following partial ordering induced by the ambiguity of locality:
\begin{eqnarray*}
b &\torder& b\\
\tau_1\funtype{\pi}\tau_2
 &\torder& 
\tau_1'\funtype{\pi'}\tau_2'
 \mbox{\ \ \ if }\tau_1'\torder\tau_1,
\tau_2\torder\tau_2',\pi\subseteq\pi'\\ 
\code{\record{$l_1$:$\tau_1$,$\ldots$,$l_n$:$\tau_n$}}
        &\torder& 
\code{\record{$l_1$:$\tau_1'$,$\ldots$,$l_n$:$\tau_n'$}}
         \mbox{\ \ \ if }\tau_i\torder \tau_i'\ (1\le i\le n)\\
\code{\bdt{$\tau$}}
        &\torder&
   \code{\bdt{$\tau'$}}
   \mbox{\ \ \ if }\tau\torder \tau'\\
\code{ref($\pi$,$\tau$)}
        &\torder&
   \code{ref($\pi'$,$\tau$)}
   \mbox{\ \ \ if }\pi\subseteq \pi'
\end{eqnarray*}
Informally, $\tau_1\torder\tau_2$ means that the locality
information of any part of type $\tau_1$ is at least as precise as
that of the corresponding part in $\tau_2$. This ordering is used to
define the typing rule for list construction:\rvsep\\ 
{\tt
\ruletwoc{{\sc (insert)}}
        {$\typing{\ass}{M_1}{\tau_1}$}
        {$\typing{\ass}{M_2}{\code{\bdt{$\tau_2$}}}$}
        {$\typing{\ass}{\code{\kwd{insert}($M_1$,$M_2$)}}
            {\code{\bdt{$\tau_3$}}}$}
	{{\rm if }$\tau_3 = \tau_1\lub\tau_2$}\rvsep\\
}
In the example of {\tt \{helen, john\}}, which is shorthand for {\tt
\kwd{insert}(helen, \kwd{insert}(john, nil))}, $\tau_1 = ${\tt
ref(\{Permanent\}, [Name:string, Age:int])} and $\tau_2 = ${\tt
ref(\{Temporary\}, [Name:string, Age:int])} and therefore we have
$\tau_1\lub\tau_1 = ${\tt ref(\{Permanent, Temporary\}, [Name:string,
Age:int])} as desired. The other rules for list types are
again standard.

The rule for assignment is also specified using the ordering
on types induced by ambiguous locality information.\rvsep\\ {\tt
\ruletwoc{{\sc (assign)}}
	{$\typing{\ass}{M_1}{\code{ref($\pi$,$\tau_1$)}}$}
        {$\typing{\ass}{M_2}{\tau_2}$}
        {$\typing{\ass}{\code{\asgn{$M_1$}{$M_2$}}}{\code{unit}}$}
	{{\rm if }$\tau_2\torder\tau_1$}\rvsep\\
}
The rationale behind this rule is that we can lose locality
information in assigning a value to a reference. 

Another expression constructor that interacts with locality information
is lambda abstraction. To give the rule for lambda abstraction, we
need to know the exact condition for a lambda term {\tt 
$\lambda$x:$\tau$.$M$} to have a function type
$\tau_1\funtype{\pi}\tau_2$ under a type assignment $\ass$. As in any
standard functional calculus, the domain type $\tau_1$ should be the
type of the lambda variable and the range type $\tau_2$ should be the
type of the body $M$ under the type assignment obtained from $\ass$ by
extending $\ass$ with the entry $x:\tau_1$.  What should be asserted
on the locality $\pi$? It should reflect the locality of the run-time
value that corresponds to the lambda term. As noted earlier in
section~\ref{func-environment}, $\pi$ has to describe the dependencies
on repositories induced by the function environment that binds a set
of variables assumed in $\ass$ to the actual parameters supplied
through function applications.

We therefore define the locality $\pi$ of the function type as the
union $\{\locality(\ass(x))|x\in dom(\ass)\}$. In the following, we
simply write $\locality(\ass)$ for the above union. The typing rule for
function abstraction is now defined as:
\rvsep\\ {\tt \ruleone{{\sc(abs)}}
       {$\typing{\ass\{x\mapsto\tau_1\}}{M}{\tau_2}$}
       {$\typing{\ass}{\lambda \code{x:}\tau_1.M}
               {\tau_1\funtype{\locality(\ass)}\tau_2}$} }

Typing rules for the other expression constructors are standard and
are summarized in Fig.~\ref{fig:typing}.
