% -*- Mode: TeX -*-

\section{Introduction}

Modern computing environments strive for several desirable features: the
environments should support the development of reliable programs, \ie,
they should be able to detect as many programming errors as early as
possible; the environments should be robust, \ie, they must gracefully
report all errors and exceptions as and when they occur; finally,
the environments should have flexible and interactive facilities for
editing, testing and debugging of programs.

Strongly typed languages meet the first goal by
guaranteeing that ``type-con\-sis\-tent'' programs will not incur run-time
type-errors.  Recent programming languages based on the Hindley/Milner
type system \cite{Damas82,Milner78} also provide the convenience of
type polymorphism and automatic type inference. But most programming
environments for such languages have to compromise the flexibility of
incremental, top-down program development in order to achieve this
``type-consistency'' over the whole program. This is because the
Hindley/Milner type system is usually formulated as a ``batch system''
that must examine the definitions before they can be used and the
complete program before any of its parts can be exercised. The problem
is further complicated due to polymorphism where the meaning of
``type-consistency'' is one of inclusion, rather than equality.

In this paper, we will address the issue of providing a robust and
interactive programming environment for Id, which is a polymorphic,
strongly typed, incrementally compiled, parallel programming language
developed at the Laboratory for Computer Science, MIT \cite{Id90}.  Id's
typing mechanism is based on the Hindley/Milner type inference system, but
it differs from its traditional description in that it is ``incremental''
in nature.  We have modified and extended the standard Hindley/Milner type
inference algorithm to facilitate incremental development and testing of
programs. In this paper, we will describe this incremental algorithm used
in Id.  We will also show its correctness (soundness and completeness) with
respect to the standard formulation of the Hindley/Milner type inference
algorithm that examines the complete program. Our goal is to produce the
same typings as obtained \via the standard algorithm, only that we produce
them incrementally.  For convenience, we will refer to the traditional type
inference mechanism as the ``batch system'' and our mechanism as the
``incremental system'' throughout the paper.

The paper is organized as follows. Section~\ref{background} discusses a
few other interactive programming environments and motivates the
incremental approach taken in Id. Section~\ref{notation} establishes
the notations used in this paper. Section~\ref{issues} describes the
issues in incremental type inference under an interactive environment
\via several examples. Section~\ref{algorithm} describes our incremental type
inference system in detail. In Section~\ref{proof} we show its
correctness. Section~\ref{extensions} extends the incremental
algorithm to handle complex editing situations. In
Section~\ref{complexity} we discuss the complexity of our system and
briefly describe some possible optimizations that are detailed in
appendix~\ref{opt-appendix}.  Finally, in Section~\ref{conclusion} we
summarize our results and compare them with the related work in this field.

