% -*- Mode: TeX -*-
\documentstyle{article}
\input{laktex}
\input{macros}

\title{Incremental Polymorphism}
\author{Shail Aditya \and Rishiyur S. Nikhil}
\date{Laboratory for Computer Science, MIT.}

\begin{document}
\maketitle

\begin{figure}[b]
\footnoterule
\footnotesize 
Current address for both authors: Laboratory for Computer
Science, Massachusetts Institute of Technology, 545 Technology Square,
Cambridge, Massachusetts 02139. Current Internet e-mail address: {\tt
shail@abp.lcs.mit.edu} and {\tt nikhil@abp.lcs.mit.edu}. 
\end{figure}

\begin{center}{\bf Abstract}\end{center}
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 first describe a general mechanism of
incremental property collection and consistency maintenance, which is
then used to maintain the types of the top-level definitions of a
program incrementally. For each occurrence of a top-level identifier,
we record its polymorphic type-scheme and the type instance generated
for that occurrence. Then, the actual type of that identifier only
needs to be maintained between these two type bounds as its definition
varies during the user session. This flexibility results from the
inherent polymorphism in the Hindley/Milner type system.  We also show
that our incremental type system is sound and complete with respect to
the more traditional ``batch system''.

We reduce the cost of incrementally editing the program by limiting
the set of affected definitions that may need to be recompiled due to
the change, and by intelligent scheduling of those recompilations in
order to amortize the cost over several such changes. Our system is
implemented and has been in use by dozens of users for more than two
years.

\end{document}
