% File: locality7.tex
% Status: Last edit by Florian 15-JAN-1990
%
\section{Summary and Further Investigations}
\label{sec:conclusions}

We have discussed the problems arising in partitioned object stores 
supporting object identity and developed a type system to formalize
and control dependencies between complex objects. The framework of
our study was a typed functional programming language enriched with
essential features of object-oriented systems like records,
(higher-order) functions and references. We developed a static type
system where the locality of an expression (i.e.\ its dependency on
repositories) is represented as part of its type and reachability
constraints among repositories are enforced by a static typing
discipline.

This work on object locality is a first step towards capturing
non-structural properties of values in a type system. Therefore, many
interesting theoretical and practical issues remain to be
investigated. We sketch some of them in the remainder of this paper.

In a static type system it is only possible to capture an
approximation of the actual locality of a run-time value. In some
cases, the estimate might be too coarse to be practical. One cause of
this is due to function closures. To obtain a sound type system, we
defined in section~\ref{func-environment} the locality of a
function closure as the possible locality of the {\em entire\/}
environment in the closure, which might contain many references that
will never be used by the function.  One possible refinement is to
consider only the set of free variables in the body of a function
definition.  

In our system a reference is always mutable in any context. In
practice, however, object identifiers would be treated in a somewhat
more controlled manner.  For example, one may not be allowed to change
objects in a certain context. In such cases, we may want to
distinguish the {\em strength\/} of the dependencies induced by
different kinds of references.  One possible approach would be to
separate object identification from mutability and to introduce
mutable and immutable reference types.

By exploiting an ordering based on the ambiguity of locality
information, we achieved a degree of flexibility in constructing
lists of values of different localities.  However, the current system
is still very restricted in that it does not allow the mixing of
references whose referred values have different localities.  For
example, suppose we have the following objects
\begin{program}
helen = \kwd{new}(Permanent, [Name = "Helen", Age = 35]);\\
john = \kwd{new}(Temporary, [Name = "John", Age = 41]]);\\
susan = \kwd{new}(Temporary, [Name = "Susan", Age = 18, Boss = helen]);\\
mary = \kwd{new}(Temporary,  [Name = "Mary", Age = 18, Boss = john]);
\end{program}% 
then the list {\tt \{helen, john\}} is legal but {\tt \{susan, mary\}}
is illegal. This restriction is needed to maintain the soundness of
the type system. However, if these references are immutable then this
restriction becomes unnecessary.  This example provides another
incentive to study immutable reference types.

Another natural extension is to include recursive types which are
essential to represent cyclic structures. One approach is to follow
\cite{Copp85,Wand84} and to use {\em regular trees\/} \cite{Cour83}
to represent recursive types.

Throughout this paper we assumed that the set ${\cal R}$ of
repositories and their reachability constraint $\mu$ are fixed and
known to the compiler. One extension that seems to be useful for
maintaining long-lived data is to allow elements of ${\cal R}$ to be
treated as values in some context. To achieve this extension without
sacrificing a static type system constitutes a
challenge. Useful techniques for this extension might be derived from
the typing discipline for modules \cite{MacQ86} and the level
distinction in a type system \cite{Card88b}.

A final extension related to the type inference method we have
described in section~\ref{sec:typeinf} is not to assume a {\em
predefined\/} reachability constraint $\mu$ but to infer a minimal (or
principal) $\mu$ a given expression satisfies.
