% File: locality5.tex
% Status: Last edit by Florian on 15-JAN-90
%
\section{Towards a Type Inference System}
\label{sec:typeinf}
The type system we have just described is based on the simply typed
lambda calculus and is too restricted to be a type system for a
practical programming language. First, it cannot represent generic
code; and second it requires tedious and often obvious type
declarations. This restriction is particularly problematic in our
system due to the need for additional locality specifications which
make programs even less generic and the required type specifications
more complicated. It is therefore essential to introduce {\em
polymorphism\/} and {\em type inference\/} into our type system. One
way to achieve this is to extend the type inference method developed
for the polymorphic programming language ML \cite{Miln78,DaMi82}. Here
we only give an informal description on how this extension can be
introduced. A full description of the system requires a certain amount
of mathematical development and is beyond the scope of this paper.
In ML, program code does not carry type specifications. The
distinguishing feature of ML's type system is that for any type
consistent {\em raw expression\/} (i.e\ an expression without type
specifications) it infers a {\em principal type scheme\/} containing
{\em type variables}. This is a type scheme such that all ground
instances obtained from it by substituting type variables with some
type terms are types of the expression, and conversely, any type of
the expression is such a ground instance. For example, for the raw
expression {\tt $\lambda$x.x} (the identity function), ML infers the
principal type scheme {\tt 'a$\func$'a} where {\tt 'a} is a type
variable. The (infinite) set of types obtainable form this scheme by
substituting {\tt 'a} with some type is exactly the set of derivable
types for the above raw expression, and therefore, the raw expression
can be used as a program of any type of the form $\tau\func\tau$. By
this mechanism, ML achieves polymorphism and relieves the programmer
of making complicated type assertions.
In order to apply this idea to our system, we need to extend ML's type
inference system in three ways. The first one is to introduce
variables for localities. The necessity of this extension is seen by
considering the raw expression {\tt $\lambda$x.!x}. According to our
typing rules, it is easily seen that this raw expression has types of
the form $\code{ref($\pi_1$,$\tau$)}\funtype{\pi_2}\tau$ for any
locality $\pi_1$ and any type $\tau$. (The locality $\pi_2$ is
determined by the type assignment.) A type scheme that represents those
types would therefore look like {\tt ref('r,'a) $\func$ 'a} where {\tt
'r} is a {\em locality variable\/} representing arbitrary localities.
This extension can be done by introducing {\em sorts\/} in the language
of type schemes, as it was done in \cite{remy89}.
Another and more difficult extension is needed to represent various
{\em constraints\/} associated with some of the typing rules in our type
system. For example, the rule {\sc (new)} for reference creation is
specified with a constraint of the form $\locality(\tau)\subseteq
\mu(R)$ saying that the locality of the argument type must be smaller
than the predefined reachability set of the repository. The rules for
{\tt $M$.$l$} (field extraction), \kwd{modify}, {\tt
\asgn{$M_1$}{$M_2$}} and \kwd{insert} are also specified with
constraints which cannot be represented by conventional type schemes.
To give the exact typing schemes to raw expressions that involve those
expression constructors, we must invent a syntactic mechanism to
represent those constraints. One approach is to refine the notion of
typing schemes to {\em conditional\/} typing schemes \cite{OhBu88}.
This is a typing scheme associated with a set of syntactic conditions
that control the instantiation of type variables. As an example, a most
general typing scheme for the raw expression {\tt
$\lambda$x.\kwd{new}(R,x)} is the following syntactic formula
\begin{program}
'a $\func$ ref({R},'a) where\{ subset(locality('a),$\mu($R$)$) \}
\end{program}%
{\tt subset(locality('a),$\mu($R$)$)} in the {\tt where} clause is a
syntactic condition on the substitution of the type variable {\tt 'a}.
A ground substitution $\theta$ {\em satisfies\/} this condition if
$\locality(\theta(\code{'a})) \subseteq \mu(R)$. A substitution
$\theta$ can be applied to the above typing scheme only if it satisfies
the condition. Under this definition the above formula represents the
precise set of types of the above raw expression. Other constraints can
also be handled by introducing appropriate syntactic conditions. We can
then apply the method developed in \cite{OhBu88} to combine these
conditions and the basic type inference methods to achieve a complete
type inference system for the type system described in this paper.
In order to obtain the full power of ML-style polymorphism, we must
combine the type inference system for our base language with the
polymorphic $let$ constructor of the form {\tt \kwd{let} $x$ = $M$
\kwd{in} $N$ \kwd{end}}. This construct allows different occurrences of
the variable $x$ in $N$ to be instantiated with different type variable
substitutions and it is the only source of ML polymorphism. The
necessary extension to include this construct is well understood for ML
\cite{DaMi82}. (See also \cite{MiHa88} for various formal properties of
the type system of \cite{DaMi82}.) However, it is known
\cite{MacQ88,Toft88} that the typing rule for \kwd{let} as defined in
\cite{DaMi82} does not agree with the operational semantics for
references and a naive mixture of references and the polymorphic
\kwd{let} results in an unsound type system. The following example is
given in \cite{MacQ88}:
\begin{program}
\kwd{let}\\
\ \ \ \=f = \kwd{new}($\lambda$x.x)\\
\kwd{in}
\> (f:=($\lambda$x.x + x), (!f)(true))\\
\kwd{end}
\end{program}%
If the type system treats the primitive \kwd{new} as an ordinary
expression constructor then it would infer the type $bool$ for the above
expression but the expression causes a run-time type error if the
evaluation of a pair is left-to-right. In \cite{Toft88,MacQ88},
solutions were proposed. They differ in details of the technical
treatment but are both based on the idea that the type system prohibits
reference values from having a polymorphic type. Either of these
solutions can be adopted by our system.
The resulting type system is particularly useful for controlling
locality. It not only enforces a predefined reachability constraint but
it also infers the exact locality information for arbitrary complex
data structures.