% -*- Mode: TeX -*-

\section{Conclusions}
\label{conclusion}
\subsection{Summary}
We have shown that it is possible to obtain correct Hindley/Milner
typings for programs of a ML-like language when placed in an incrementally
compiled environment geared towards easy editing, debugging and testing.
Our approach is guided by Lisp-like environments that offer definition
level incrementality and dynamic linking. A single toplevel definition
forms a convenient unit of compilation and inter-unit consistency
maintenance both in terms of maintaining modularity and minimizing
book-keeping overhead. 

We have achieved this incremental flexibility by maintaining the
interface of a top-level definition with respect to the other
definitions in a consistent fashion. We described a general mechanism
of incremental property collection and consistency maintenance, which
was applied in our case to maintaining the types and the strongly
connected components of top-level definitions of a program. We took
advantage of the inherent polymorphism of the type system by keeping
only the upper and lower bounds of type usage and maintaining the
definitions within those bounds.

We should mention that the automatic, incremental book-keeping mechanism
we described in the preceding pages is independent of the program
granularity it is applied to. It could very well be applied to program
modules consisting of groups of definitions, or to complete files, or at a
finer grain, to individual subexpressions inside a top-level
definition. 

\subsection{Comparison with Related Work} 

Some other systems \cite{Meertens83,PoplogV14,Toyn87} also provide
incremental compilation. The GLIDE system \cite{Toyn87} comes closest
to our philosophy of incremental type inference because it is also
based on the ideas presented by Nikhil in \cite{Nikhil85}, but it
differs significantly in approach. 

The GLIDE system employs an automatic, lazy loading strategy at
run-time whereby definitions are automatically compiled and loaded
into the run-time environment only as needed by the currently
executing expression. It also does retyping of old definitions on the
fly, if necessary.  In sharp contrast, our system has clearly
distinguishable phases of compilation, loading, consistency checking,
and execution.  Each phase is explicitly initiated by the user which
gives him/her complete control over scheduling of various definitions
through the individual phases.

The lazy loading mechanism of GLIDE has the advantage of touching
only those definitions that are actually needed at run-time, but it
forces the system to perform all the necessary consistency checks and
resulting retypings immediately as each new definition is loaded.
This must be done in order to detect any fresh type errors caused by
the changed or new definition before the execution can resume.  As
pointed out in section~\ref{complex}, such a strategy may end up
in quadratic number of retypings for programs resembling the example
in \fig{dag-chains} (c).  The GLIDE system attempts to reduce the work
involved in such retypings by sharing type information between
multiple retypings of the same definition. 

In contrast, our system permits early loading of definitions and puts
all retyping under explicit user control. The user is guided by the
errors reported during consistency checking in appropriately
scheduling the retypings so that no definition needs to be retyped
more than once. Note that the consistency checks now have to be
performed for each definition in the static call graph of the query
expression rather than the definitions actually used in its
execution. 

Probably the most important difference between our system and the
GLIDE system is in the actual framework for consistency checking and
maintenance. We have been able to formalize an independent system of
incremental property maintenance, and have used it successfully to
maintain type and SCC properties of top-level definitions. The GLIDE
system, on the other hand, has a specific incremental type inference
system built into it. Our type consistency checks use the inherent
polymorphism of the language to advantage and avoid retyping where
simple syntactic interference checks as used in GLIDE may not be able
to do so. And finally, we collect and maintain incremental type
information only at the granularity of top-level definitions and no
record is kept for internal subexpressions. The GLIDE system, on the
other hand, maintains type information at all subexpressions so that
it may be reused during retyping.

\subsection{Status}
Finally, we should point out that the incremental type inference
system for Id described in this paper has been implemented in the Id
compiler and has been in use for the last two years.

\section{Acknowledgements} 

We would like to express our thanks to Zena Ariola, Boon Ang, Alejandro
Caro, and Steve Glim, from the Computation Structures Group
at Laboratory for Computer Science, MIT, for their insightful comments
and help in proof-reading this paper.
