% -*- Mode: TeX -*-

\section{Extensions to Algorithm $W_{1}$}
\label{extensions}

\subsection{Complete Programs}

Uptil now we dealt with a given set of top-level definitions supplied
incrementally that were assumed to form a complete program. Actually,
the notion of a complete program depends on the program query. Only
those definitions that are called by the program query, directly or
indirectly, need to be supplied and checked for consistency. The
status of other definitions that are unrelated to the given query, is
unimportant.  Therefore, in the incremental system, we perform the
consistency checks only for the minimal set of definitions that are
self contained with respect to the given program query. This set can
be computed by looking at the minimal call graph rooted at the given
query, that does not have any dependency edges going out of it.  This
can enormously reduce the number of definitions that need to be checked.

\subsection{Constraint Relaxation}

The other problem that we have not yet addressed is editing that leads
to constraint relaxation. The completeness lemma~\ref{TEi-TEt}
implies that the compilation environment of the incremental system is
never allowed to be more constrained than the final environment of
the batch system. This may not always be the case due to editing when
some constraints on the bindings may get relaxed as shown in
section~\ref{relax}.  It is the user's responsibility to recompile a
definition after editing it, but it is the compiler's responsibility
to propagate those changes throughout the rest of the program and warn
the user accordingly while maintaining soundness and completeness of
the derived types.

We can detect these constraint relaxations by using 
some additional property assumptions and checks as defined below. We
can collect these extra assumptions along with the upper bound type
assumptions already collected in algorithm $W_1$.

\begin{figure}
\begin{tabular}{|p{\hlessm}|}
\hline
\illustration{type-relax} \\
\parbox{\hlessm}{(a): Using the Lower Bound Assumptions (N) to
detect type constraint relaxation for definition \tbx{g}.} \\
\hline
\illustration{scc-relax} \\
\makebox[\hlessm]{(b): Using the SCC Assumptions (Q) to detect reduced
SCCs for definition \tbx{t}.} \\
\hline
\end{tabular}
\caption{Examples of additional assumptions being used to detect
Constraint Relaxation during editing.}
\label{fig:relax}
\end{figure}

\begin{description}
\item[Assumption] -- We define an assumption domain ${\cal N}$ called
the {\it Lower-Bound-Type-Assumptions} that is used to 
record the actual type-schemes of free generic
identifiers used within a top-level definition.
\begin{equation}\begin{array}{l}
\bx{COLLECT:} \;\;N_x=\{y\mapsto{}\fn{TE}{y}\},\hmm\forall{}y\in{}(\fn{free}{e_x}-SCC_x) \\
\bx{CHECK:} \;\;\forall (y\mapsto{}\sigma_y) \in N_x,\;\sigma_y \succeq \fn{TE}{y}
\end{array}\end{equation}
These assumptions are called the lower bound type assumptions because
the recorded assumee type-scheme is a lower bound for the assumee type
instances used by the assumer according to the partial order of the
type domain. Note that the assumption check uses the same subsumption
test as for the upper bound type assumptions, but in the reverse
direction. The check fails if the assumee type-scheme becomes more
polymorphic than it was assumed to be when the assumer was compiled. 
This enables the assumer to be flagged for recompilation in order to
adjust its type according to the latest assumee type-scheme.

\item[Assumption] -- We also define an assumption domain ${\cal Q}$
called {\it SCC-Assumptions} that is used to record the SCC of each
identifier used directly by another identifier from within its own
SCC.
\begin{equation}\begin{array}{l}
\bx{COLLECT:} \;\;Q_x=\{y\mapsto{}SCC_y\},\hmm\forall{}y\in{}(\fn{free}{e_x}\cap{}SCC_x) \\
\bx{CHECK:} \;\;\forall(y\mapsto{}SCC_y)\in{}Q,\;SCC_y=\fn{SE}{y}
\end{array}\end{equation}
The consistency check in this case is a test of (set) equality. This
ensures that if the SCC of one of the identifiers changes, then all
identifiers that were excluded from its old SCC during this change
will fail this check and will be flagged for recompilation. 
\end{description}

To see how these additional assumptions help in detecting constraint
relaxation, we apply them to the examples given earlier in
section~\ref{relax}. 

The situation for the first example of section~\ref{relax} is
pictorially depicted in \fig{relax} (a). The function \tbx{g} uses
function \tbx{f} with type instance {\tt (int -> int -> int)} derived
from its initial type-scheme {\tt (int -> *0 -> int)} which is
recorded in the lower bound assumption set of \tbx{g}. After function
\tbx{f} is edited, its new type-scheme becomes {\tt (*1 -> *0 -> *1)}
which fails the lower bound assumption check against the type-scheme
recorded in \tbx{g}'s lower bound assumption set. Therefore, the
system will be able to flag the recompilation of function \tbx{g}, so
that it may benefit from the relaxed type of function \tbx{f}. Note
that this type relaxation of \tbx{f} can not be detected \via the
upper bound type assumptions of \tbx{g} because \tbx{f}'s type
instance recorded there remains an instance of the relaxed type-scheme
of \tbx{f}.

Looking at the second example given in section~\ref{relax} (see
\fig{relax} (b)), the function \tbx{t} records the SCC of the function
\tbx{h}, \tbx{\{h,t\}}, in its SCC assumption set. After \tbx{h} is
edited, its new SCC, \tbx{\{h\}}, fails the SCC assumption check
against the earlier value recorded in the SCC assumption set of
\tbx{t}. Thus, the system will be able to flag the recompilation
of function \tbx{t} which will relax its type and SCC properties to
their correct values. 

Our new termination strategy is now only slightly more complex.  

\begin{term-strategy}\label{edit-strategy} To test for termination of the extended
incremental system, we execute the following steps.
\begin{tightenum}
\item  Build a static call graph with the query binding 
 ``$\tbx{it}=e_{\sibx{main}}$'' as the root.
\item  Check if any leaf identifier from the above call
graph has not yet appeared for compilation.
\item Check if the upper bound type assumptions (M), the lower bound
type assumptions (N), and the SCC assumptions (Q)  for each
identifiers in the call graph are all satisfied in the latest
compilation environment.
\item If all the above tests are passed, then the incremental system terminates.
\end{tightenum}
\end{term-strategy}

Our incremental type inference system is now complete. We use all the
assumption domains ${\cal M}$, ${\cal N}$, and ${\cal Q}$, and the
termination strategy~\ref{edit-strategy} in the overall plan of
\fig{flowchart}, while using the algorithm $W_1$ to process each
top-level binding. We can type-check a set of definitions
incrementally, allowing editing of earlier definitions. The additional
assumption domains ${\cal N}$ and ${\cal Q}$ make sure that the types
inferred are both sound and complete even with arbitrary editing.

