% -*- Mode: TeX -*-

\section{Complexity and Optimizations}
\label{complexity}

\subsection{Complexity of the Incremental System}
\label{complex}
Apart from the inherent complexity of the Hindley/Milner type system,
which is known to be exponential \cite{Mairson90}, our incremental
system incurs book-keeping and recompilation overheads. The
book-keeping cost can be included within the regular cost of compiling
a program. Therefore, we will only focus on the number of recompilations
necessary in our incremental system to arrive at the correct typings.

Incremental changes in the program potentially affect all the
topologically preceding definitions starting from the point of change
in the call graph. Our mechanism of maintaining upper and lower bound
assumptions attempts to reduce this set of affected definitions.  When
the definition of an identifier appearing later in the incremental
sequence of compilations falls within the assumed bounds, no
recompilation is flagged. Even when these assumptions fail, we can
localize the retyping to just the assumer identifier and its SCC
instead of the whole program.  But, in the worst case, each such
recompilation can give rise to more failures in the topologically
preceding SCCs and we may end up recompiling the whole program.

\begin{figure}
\begin{tabular}{|p{\hthirdmmm}p{\hthirdmmm}p{\hthirdmmm}|}
\hline
\multicolumn{3}{|p{\hlessm}|}{\illustration{dag-chain}} \\
\makebox[\hthirdmmm]{(a)} &
\makebox[\hthirdmmm]{(b): Static Call Graph.} &
\makebox[\hthirdmmm]{(c)} \\
\hline
\end{tabular}
\caption{Example program to illustrate the high number of
Recompilations.}
\label{fig:dag-chains}
\end{figure}

As an example, consider the set of definitions given in
\fig{dag-chains} (a).  The call graph in this case is a simple chain
as shown in (b). The upper bound type assumptions of the identifier
\tbx{h} fail the assumption checks as soon as \tbx{m} is defined, and
\tbx{h} has to be recompiled. The recompilation of \tbx{h} propagates
the type information of \tbx{m} onto \tbx{h} and causes the failure of
assumption checks of \tbx{g} and so on. This example shows that the
cost of an incremental change to the program could be linear in its
size.

Recompiling a definition as soon as some of its assumptions
fail, may not be the best strategy. The definitions given in
\fig{dag-chains} (c) will incur quadratic number of recompilations
following this strategy, because every time a new definition is
encountered, the upper bound type assumptions of all the preceding
definitions fail. It is possible to amortize the cost of recompilation
over several assumption failures by adopting a lazy recompilation
strategy. If we postpone all recompilations until all the definitions
have been encountered, a single sweep of recompilations in the reverse
order will settle all the types to their correct values. We have
adopted this lazy strategy in Id by postponing all recompilations
until we are ready to evaluate a program query (see \fig{flowchart}).


\subsection{Optimizations}
\label{optimize}
It is possible to further reduce the cost of an incremental change to
the program, if it does not affect the properties of other nodes. In
our current scheme, whenever a node is flagged for recompilation, we
recompile all the definitions in its latest SCC. This is necessary
when the new SCC of the node is different from its old one. But this
may be wasteful if the editing changes do not affect the SCC or the
type properties of the node. Indeed, the only computation really
necessary in such cases is the compilation of the edited node itself.

Even when the type of the edited node is different but its SCC is the
same, it may not be necessary to recompile all the other definitions
in its SCC.  This is because type-checking a given definition does
not use any information about other definitions in its SCC (apart
from the fact that they are all in the same SCC) until the latter
part of algorithm $W_1$ when we unify all the assumed types of the
definitions with their computed types in a unification matrix (see
\fig{algo-w1}).  Therefore, if we save the assumed types of SCC
identifiers while typing a given definition, we can use them directly
in the latter part of the $W_1$ algorithm when some other identifier
from the same SCC is being recompiled. The details of these
optimizations and a modified inference algorithm $W_2$ appear in
appendix~\ref{opt-appendix}.
