% -*- Mode: TeX -*-

\begin{abstract}
The Hindley/Milner polymorphic type system has been adopted in many
programming languages because it provides the convenience of programming
languages like Lisp along with the correctness guarantees that come with
static type-checking. However, programming environments for such languages
are still not as flexible as those for Lisp. In particular, the style of
incremental, top-down program development possible in Lisp is precluded
because the type inference system is usually formulated as a ``batch
system'' that must examine definitions before their uses. This may require
large parts of the program to be recompiled when a small editing change is
performed.

In this paper, we attempt to strike a balance between the apparently
conflicting goals of incremental, top-down programming flexibility and
static type-checking. We present an incremental typing mechanism in which
top-level phrases can be compiled one by one, in any order, and repeatedly
(due to editing). We show that the incremental type system is sound and
complete with respect to the more traditional ``batch system''. The system
derives flexibility from the inherent polymorphism of the Hindley/Milner
type system and minimizes the overhead of book-keeping and recompilation.
Our system is implemented and has been in use by dozens of users for more
than two years. 
\end{abstract}
