% -*- Mode: TeX -*-

\section{The Incremental Type Inference System}
\label{algorithm}

Our incremental system is based on the standard Hindley/Milner inference
rules given in the literature \cite{Damas82,Clement86,Tofte88}, so
we will not describe those inference rules again. We follow the
description of \cite{Tofte88} which expresses the rules for
Instantiation and Generalization implicitly. This has the advantage of
making the inference rules completely deterministic\footnote{This
means that exactly one rule will apply to a given expression.}, and we
always infer a type for an expression instead of a
type-scheme\footnote{The equivalence of the rules appearing in
\cite{Damas82} and those in \cite{Tofte88} has been shown in
\cite{Clement86}.}.

In this section, we will describe our incremental book-keeping
strategy and the incremental type inference algorithm that uses it.

\subsection{Incremental Book-Keeping}

The basic idea in incremental compilation is to be able to compute
some desired compile-time properties for an aggregate of identifiers
in an incremental fashion. This aggregate forms the {\bf identifier
namespace} that we operate in. For our purposes, this is the set of
all top-level identifiers. Our first step is to define a ``property''.

\begin{definition}\label{property} A {\bf property} ${\cal P}=({\cal
D},\sqsubseteq)$ is characterized by a domain of values $\cal D$
partially ordered\footnote{A partial order on a domain is a reflexive,
transitive, and anti-symmetric binary relation on the elements of the
domain.} by the relation $\sqsubseteq$. Given two values, $v_1,v_2 \in
{\cal D}$ for a property ${\cal P}=({\cal D},\sqsubseteq)$, we say
that $v_1$ is consistent with $v_2$ if and only if $v_1\sqsubseteq{}v_2$.
\end{definition}

The domain of values is simply a syntactic set of values with some
structural relationship defined among its elements.  The domain must also
contains a special element ``$\bot$'' (read ``bottom'') that corresponds to
the default property value assigned to as yet undefined identifiers in the
namespace. 

The interdependences among the properties of identifiers at various
times during incremental compilation is maintained \via sets of
``assumptions'' defined below.

\begin{definition}\label{assumption} An {\bf assumption}
$(x,y,v_y)\in{\cal A}$ is a triple consisting of an {\bf assumer} $x$,
an {\bf assumee} $y$, and an {\bf assumed-value} $v_y\in{\cal D}$, for
the assumee's property ${\cal P}=({\cal D},\sqsubseteq)$. ${\cal A}$
is termed as the {\bf assumption domain}. An {\bf assumption set}
$A_x$ for the assumer $x$ is a set of all such assumptions made by $x$
and can be written as a map from the assumees to their assumed-values.

Each assumption domain has an associated consistency checking
function. An {\bf assumption check} $C$ is a predicate that verifies
the assumed-value $v_y$ of an assumee from a given assumption set against
its current value $v_y'$ available in the environment for consistency. 
This check may use the property predicate $\sqsubseteq$ for this purpose.
\end{definition}

Assumption domains are characterized by the properties they record and
the assumption checks they employ in order to verify consistency.
Several assumption domains may be associated with the same property
that use different assumption checks. We will see examples of this
later on. Also note that an assumption set for an assumer may contain
several assumptions for the same assumee corresponding to its various
occurrences in the definition of the assumer. 

The union of all the property mappings of namespace identifiers to their
property values constitutes a {\bf compilation environment}.  The sets of
assumptions associated with each assumer identifier make up the
book-keeping overhead of the compilation environment.

\subsection{Overall Plan for Incremental Analysis}
\label{overall-plan}

\begin{figure}
\begin{boxit}
\illustration{flowchart}
\end{boxit}
\caption{Overall Plan for Incremental Property Maintenance.}
\label{fig:flowchart}
\end{figure}

The overall scheme for incremental property computation and
maintenance appears in \fig{flowchart}. Essentially, we process each
top-level binding individually, accumulating its assumptions and
property values in the current environment. If we need to evaluate a
query, we first check whether all the accumulated assumptions are
consistent with respect to the latest environment, and proceed to
evaluate the query only if all the assumptions pass their checks.
Otherwise, the failing definitions are flagged for recompilation.

The success or failure of the above mechanism in computing the desired
properties correctly and efficiently depends upon several factors.
These factors include, the semantic characteristics of the accumulated
property domains, their interdependences and computation algorithms,
the various kinds of assumptions collected and their respective
assumption checks, and the incremental compilation environment history
and its maintainance.  Now, we will use this incremental property
maintenance strategy to compute the types of top-level definitions
within the well defined framework of Hindley/Milner type inference
system.

\subsection{Properties and Assumptions}

\begin{figure}
\begin{boxit}
\illustration{properties}
\end{boxit}
\caption{Compilation Properties used in the Incremental System.}
\label{fig:props}
\end{figure}

\begin{figure}
\begin{boxit}
\illustration{assumptions}
\end{boxit}
\caption{The Upper Bound Type Assumptions used in the Incremental
System.}
\label{fig:assp}
\end{figure}

As a start, we consider only out-of-order compilations, \ie, we will assume
that editing of previously defined bindings is not permitted, though, new
bindings can still be added incrementally.  This is done to ensure
monotonicity of the compilation environment and will be relaxed in a later
section.  We still allow the compiler to issue recompilations of previously
encountered bindings if necessary, but the user is not allowed to edit
them.

We maintain the following compilation properties and assumptions in
this system.

\begin{description}
\item[Property] -- $\ibx{Type} = (\bx{Type-Schemes},\succeq)$
(see \fig{props} (a)). This property records the type of all the
identifiers. The ``bottom'' element of the domain is the most general
type-scheme $\forall\alpha.\alpha$. As stated earlier, we
denote the mapping of identifiers to their types in a Type-Environment (TE).

\item[Property] -- $\ibx{Strongly-Connected-Components} =
(\fn{powerset}{\bx{Identifiers}},\subseteq)$ (see \fig{props} (b)). The
{\em strongly connected component} (SCC) of an identifier is the set of all
identifiers in the static call graph that are mutually recursive with the
given identifier. We denote the mapping of the identifiers to their
recursive sets in a SCC-Environment (SE).

\item[Assumption] -- We define an assumption domain ${\cal M}$ called
the {\it Upper-Bound-Type-Assumptions} that is used to record
the actual type instance of each use of a free generic identifier in a
top-level definition (see \fig{assp}).
\begin{equation}\begin{array}{l}
\bx{COLLECT:} \;\;M_{x} = \{(y\mapsto{}\tau_{y})\},\hm\forall\;
\bx{occurrences of}\;y\in(\fn{free}{e_{x}}-\ibx{SCC}_{x}) \\
\bx{CHECK:} \;\;\forall (y\mapsto{}\tau_y) \in M_x,\; \fn{TE}{y}\succeq\tau_y
\end{array}
\end{equation}
These assumptions are called the upper bound type assumptions because
in the partially ordered domain of type instances of the assumee's
type-scheme, the recorded instances appear as an upper bound of useful
instances used by the assumer.  We collect a set of such assumptions
for each assumer identifier defined on the left hand side of a
top-level binding. The associated assumption check tests if these
assumed types are valid instances of the latest type-scheme assigned
to the assumee identifiers in some later type environment \ibx{TE}.
\end{description}

The upper bound type assumption checks ensure that the final type-scheme of
an assumee identifier in the environment \ibx{TE} is at least as
polymorphic as it was assumed when its assumer definition was compiled. If
any of these checks fail, we may conclude that the assumee's type-scheme
has changed significantly since the compilation of its assumer, and
therefore, the assumer definition should be recompiled. For example, after
the second redefinition of function \tbx{g} in section~\ref{edit}, its
latest type {\tt (int -> int)} can no longer instantiate the assumed type
{\tt (int -> (list int))} recorded in the upper bound type assumptions of the
function \tbx{f}, which will then be flagged for recompilation by the
system.

\subsection{Incremental Algorithm}

Our identifier namespace consists of the set
$X=\{x_1,x_2,\ldots,x_n\}\cup\{\tbx{it}\}$ of identifiers bound in the LHS
of the top-level bindings in a complete program as defined by
equation~\ref{complete-program}. The initial property environments
TE$_0$ and SE$_0$, assign the bottom elements of their respective
domains to all the identifiers in the namespace.

\begin{implication}
& \rjust$\ibx{TE}_0$ & $=$ & $\ibx{TE}_{\sibx{lib}}\cup\{x_k\mapsto\forall\alpha.\alpha\}$ & $\forall{}x_k\in{}X.$ & \proofrefcount{TE-init-eq} \\
& \rjust$\ibx{SE}_0$ & $=$ & $\{x_k\mapsto\phi\}$ & $\forall{}x_k\in{}X.$ & \proofrefcount{SE-init-eq}
\end{implication}

TE$_0$ also includes a standard library type environment
$\ibx{TE}_{\sibx{lib}}$ that maps 
all the standard library function identifiers, predefined operators
\etc. to their appropriate type-schemes. There are no free type-variables
in this environment by assumption.

\begin{figure}
\begin{tabular}{|p{\hlessm}|}
\hline
\begin{display}
\tbx{Def} W$_1$(TE$_{i-1}$,SE$_{i-1}$,B$_i$) =
    Let $B_i$ be the binding `$x = e_x$'.
    Construct the current call graph $G_i$ using the free identifiers of B$_{i}$.
    Let $SCC_x^i=\{z_1,\ldots,x,\ldots,z_n\}$ be the current SCC of $x$ in $G_i$.
\vsp
    SCC Environment: 
        $\ibx{SE}_i{}=\ibx{SE}_{i-1}\setminus_{SCC_x^i}+\{z_k\mapsto{}SCC_x^i\}$                  $\forall{}z_k\in{}SCC_x^i$.
\vsp
    \tbx{for each} top-level identifier $z_k\in{}SCC_x^i$ \tbx{do}
        Let $e_{z_k}$ be the RHS expressions associated with $z_k$.
        Let $\beta_{k1},\ldots,\beta_{kn}$ be new type-variables.
        $\ibx{New-TE}_k^i=\ibx{TE}_{i-1}\setminus_{SCC_x^i}+\{z_1\mapsto\beta_{k1},\ldots,z_n\mapsto\beta_{kn}\}$.
        $(S_k^i,\tau_{z_k}^i,A_k^i)=W'(\ibx{New-TE}_k^i,e_{z_k})$.
    \tbx{endfor}.
\vsp
\end{display} \\
\hspace*{1.25em}$U_i=\ibx{Unify-Columns}\left(\begin{array}{ccccc}
                S_1^i(\beta_{11}) & \cdots & S_1^i(\beta_{1k}) & \cdots & S_1^i(\beta_{1n}) \\
                         \vdots   &        &     \vdots        &        &     \vdots        \\
                S_n^i(\beta_{n1}) & \cdots & S_n^i(\beta_{nk}) & \cdots & S_n^i(\beta_{nn}) \\
                \tau_{z_1}^i      & \cdots & \tau_{z_k}^i      & \cdots & \tau_{z_n}^i      
                            \end{array}\right)$ \\
\begin{display}
    Type Environment: 
        $\ibx{TE}_i=\ibx{TE}_{i-1}\setminus_{SCC_x^i}+\{z_k\mapsto\fn{close}{U_i\tau_{z_k}^i}\}$         $\forall{}z_k\in{}SCC_x^i$.
\vsp
    Upper-bd Type Assumptions: 
        $M_{z_k}=U_i{}A_k^i\setminus_{SCC_x^i}$                                      $\forall{}z_k\in{}SCC_x^i$.
\vsp
  \tbx{Return} $(\ibx{TE}_i,\ibx{SE}_i)$.
\vsp
\end{display} \\
\hline
\end{tabular}
\caption{The Incremental Algorithm $W_1$.}
\label{fig:algo-w1}
\end{figure}

\begin{figure}
\begin{tabular}{|p{\hlessm}|}
\hline
\begin{display}
   \tbx{Def} $W'$(TE,e) =
     \tbx{case} e \tbx{of}
       x            $\Rightarrow$ \tbx{let} 
                           $\forall\alpha_1\cdots\alpha_n.\:\tau=\fn{TE}{x}$.
                           $\beta_1,\ldots,\beta_n$ be new type-variables.
                           $\tau'=\{\alpha_i\mapsto\beta_i\}\tau$.
                        \tbx{in}
                           (ID,$\tau'$,$\{(x\mapsto\tau')\}$).
       $\lambda{}x.\:e_1$      $\Rightarrow$ \tbx{let} 
                           $\beta$ be a new type-variable.
                           $\ibx{TE}' = \ibx{TE}+\{x\mapsto\beta\}$.
                           $(S_1,\tau_1,A_1) = W'(\ibx{TE}',e_1)$.
                        \tbx{in}
                           $(S_1,S_1\beta\rightarrow\tau_1,A_1\setminus_{\{x\}})$.
       $e_1$ $e_2$       $\Rightarrow$ \tbx{let} 
                           $(S_1,\tau_1,A_1) = W'(\ibx{TE},e_1)$.
                           $(S_2,\tau_2,A_2) = W'(S_1(\ibx{TE}),e_2)$.
                           $\beta$ be a new type-variable.
                           $S_3 = U(S_2\tau_1,\tau_2\rightarrow\beta)$.         (may {\bf fail})
                        \tbx{in}
                           $(S_3S_2S_1,S_3\beta,S_3(S_2A_1\cup{}A_2))$.
       \tbx{let $x = e_1$ in $e_2$} $\Rightarrow$ 
                        \tbx{let}
                           $(S_1,\tau_1,A_1) = W'(\ibx{TE},e_1)$.
                           $\ibx{TE}' = S_1(\ibx{TE}) + \{x\mapsto\ibx{close}(S_1(\ibx{TE}),\tau_1)\}$.
                           $(S_2,\tau_2,A_2) = W'(\ibx{TE}',e_2)$.
                        \tbx{in}
                           $(S_2S_1,\tau_2,S_2A_1\cup{}A_2\setminus_{\{x\}})$.
     \tbx{endcase}. 
\end{display} \\
\hline
\end{tabular}
\caption{Pseudo-code for the Inference Algorithm $W'$.}
\label{fig:algo-w'}
\end{figure}

Our incremental type inference algorithm\footnote{The notation
$A\setminus_{B}$ used in the algorithm represents the mapping $A$ with
its domain restricted to elements other than those in set $B$.} $W_1$
appears in \fig{algo-w1}.  This algorithm corresponds to the
\ibx{process-binding} function of \fig{flowchart}.  With each
invocation of $W_1$, we compute the compilation properties and the
assumptions of a single top-level binding and accumulate them in the
compilation environment.

The first step in algorithm $W_1$ is to compute the static call
graph\footnote{A {\bf Static Call graph} is a directed graph where each
top-level binding is a node, and there is an edge from binding $x=e_x$ to
binding $y=e_y$ in the graph whenever there is an occurrence of $y$ inside
$e_x$, or in other words, whenever $x$ \ibx{uses} $y$.} of the current binding
$x=e_x$ (also denoted by $B_i$, corresponding to the $i$-th invocation of
$W_1$), using the currently reachable nodes. Then, we partition this graph
into its strongly connected components using standard graph theoretic
techniques \cite{Aho74}.  We record the strongly connected component
$SCC_{x}^{i}$ for the top-level identifier $x$ within
the SCC environment.  

In our incremental system, we treat all the bindings
contained within a SCC as a single \ibx{supernode} of the static call graph
and type all of them together, each time any one of them changes. This is
necessary in order to correctly identify and type the definitions that become
mutually recursive incrementally.  For instance, the examples of
section~\ref{recurse} will all be typed correctly when the last definition
in their strongly connected component is encountered. This may require
keeping track of the actual code of each definition as it is compiled,
which is not too difficult to maintain in the integrated
editor-compiler environment of Id.

The set of bindings $z_k=e_{z_k}$ for each $z_k\in{}SCC_x^i$ are
type-checked in two phases. First, we type-check each of the RHS
expressions $e_{z_k}$ independent of the types of other top-level
identifiers of $SCC_x^i$. We also collect upper bound type assumptions for
each $z_k$ from its RHS. Then in the second phase, we unify the defined type
$\tau_{z_k}^i$ obtained from typing each RHS, with the type of $z_k$
as used by other bindings of the same SCC.  We do this operation as one giant
unification of all the terms corresponding to the same top-level
identifier. This operation effectively simulates the task of the fixpoint
constructor necessary to model recursive definitions in the batch system.

The algorithm $W'$ that actually computes the type of each top-level RHS
expression and records its type assumptions, is shown in \fig{algo-w'}. It
recursively collects all type instances generated for each use of a freely
occuring identifier into a set of type assumptions for the current assumer.
We will show some assertions about these collected assumptions in the next
section.  Apart from this extra book-keeping, the algorithm is exactly the
same as the standard type inference algorithm $W$ of \cite{Tofte88}.
Consequently, the theorems of soundness and completeness of the type
computed by $W$ with respect to the standard Hindley/Milner inference rules
(see \cite{Damas82,Tofte88}) are also valid for $W'$.
