% -*- Mode:TeX -*-

\section{Issues in Incremental Typing}
\label{issues}

In this section, we will describe the various issues that need to be
addressed during incremental type inference by means of simple
examples\footnote{Even though all our analysis is based on the
mini-language given in section~\ref{notation}, our examples use the
full Id syntax for convenience and clarity.  In \cite{Gupta90}, we
show a simple translation from Id to this mini-language.}.

\subsection{Forward References}
\label{forw}
In Id, all top-level definitions are compiled into a single
global environment. So, it is possible and convenient to use
functions that are defined later, as the following example
shows\footnote{In Id, toplevel function
definitions are introduced with the keyword \tbx{def} and terminated by
a semi-colon (\tbx{;}). Also, colon (\tbx{:}) is the infix cons
operator. Text following a percent (\tbx{\%}) is taken to be a comment and
is ignored.}:

\begin{code}
def f x = (x+1):(g x);                \% int -> (list int)
\vsp
def g x = x:nil;                      \% *0 -> (list *0)
\end{code}

We have shown the inferred type for each of the definitions as a comment
appearing to the right of the definition\footnote{The type variables
appearing in a type are assumed to be implicitly universally quantified at
the outermost unless otherwise stated or clear by the context.}.  Assuming
that the above definitions are compiled in the order of their appearance,
the function \tbx{f} uses \tbx{g} inside its body as a
function with type {\tt (int -> (list int))} without actually knowing
anything about it.

When \tbx{g} is compiled, \tbx{f} ``sees'' its definition and the system
should make sure that all its previous uses are ``consistent'' with its
definition. In later sections, we will describe in detail how this
consistency check is formulated and verified. For now, it suffices to say
that use of an identifier should have a type that is an instance of the type
inferred at its definition.  In the above example, it is indeed the case,
the type of \tbx{g}, {\tt (int -> (list int))}, used within \tbx{f} is an
instance of the defined type of \tbx{g}, {\tt (*0 -> (list
*0))}\footnote{This instantiation uses the simple substitution $S=\{{\tt
*0} \mapsto {\tt int}\}$ for the bound type-variable {\tt *0}.}. Therefore,
\tbx{f} need not be recompiled even though it used \tbx{g} before it was
defined.

\subsection{Editing}
\label{edit}
Going a step further, we may edit \tbx{g} as follows:

\begin{code}
def g x = x:(x-1):nil;                \% int -> (list int)
\end{code}

This restricts the type of \tbx{g}, but its use inside \tbx{f} is still
valid, and no recompilation is necessary.  On the other hand, if we had
redefined \tbx{g} as,

\begin{code}
def g x = x-1;                        \% int -> int
\end{code}

\hspace*{-\parindent} then the inferred type of \tbx{g} no longer matches
its use inside \tbx{f} and the system should detect it and
report an error.  Note that this analysis is independent of the order
of the original definition of \tbx{f} and \tbx{g}, or for that matter, any
other definitions that appear temporally in between the
definitions of \tbx{f} and \tbx{g}. Such independent definitions are
never disturbed; all recompilation requirements, if any, apply only to
the definitions that fail the consistency check.

\subsection{Mutual Recursion}
\label{recurse}
The situation becomes more complicated with mutually recursive
functions, which have to be type-checked together in the
Hindley/Milner type system. In the incremental system, such definitions
may be compiled separately. We have to either rule out such cases by
requiring that mutually recursive definitions be supplied together, or
incrementally detect definitions that become mutually recursive and
handle them appropriately.  Simple book-keeping, as described in
section~\ref{forw}, may fail to catch type-errors embedded across
mutually recursive definitions, as the following example shows:

\begin{code}
def f x = g f;                        \% *0 -> *1
$\cdots$
def g x = f g;                        \% *2 -> *3
\end{code}

The above two definitions are mutually recursive and are rejected by
the batch system\footnote{The Hindley/Milner type system does not
handle infinite types and flags them as type-errors.  In this example,
the type of both \tbx{f} and \tbx{g} are infinite.}. The incremental
system infers the type of \tbx{f} to be {\tt (*0 -> *1)}, as shown
above, assuming the type of \tbx{g} to be {\tt (*0 -> *1) -> *1)}.
Similarly, when \tbx{g} is compiled, its type is obtained as {\tt (*2
-> *3)}, assuming the type of \tbx{f} to be {\tt ((*2 -> *3) -> *3)}.
Note that in both cases, the assumed types are instances of their
corresponding inferred types, and the simple consistency checking
used in section~\ref{forw} is not sufficient to catch the type-error
in the above program. 

The following example shows that without explicit book-keeping of
mutually recursive definitions, the incremental system may, in
fact, compute unsound types even when there is no overall type-error.

\begin{code}
def K x y = x;                        \% *0 -> *1 -> *0
\vsp
def f x = (g f) x;                    \% *2 -> *3
\vsp
def g x = K x (x:(f x));              \% *4 -> *4
\end{code}

The \tbx{K} function simply returns its first argument. The inferred types
of \tbx{f} and \tbx{g} individually are as shown.  The uses of both \tbx{f}
and \tbx{g} are instances of their inferred types, so no consistency error
is present. But when supplied together and taking into account that \tbx{f}
and \tbx{g} are mutually recursive, the correctly computed Hindley/Milner
type of \tbx{g} should be {\tt ((*4 -> (list *4)) -> (*4 -> (list *4)))}
and that of \tbx{f} should be {\tt (*4 -> (list *4))}.

\subsection{Editing and Type Relaxation}
\label{relax}
It is possible during editing that the type of
a definition gets relaxed and therefore must be reflected in other
definitions that use it. Consider the following example:

\begin{code}
def f x y = (x+1);                    \% int -> *0 -> int
\vsp
def g x y = f x (y+1);                \% int -> int -> int
\end{code}

The type of \tbx{f} constrains the type of \tbx{g}'s argument
\tbx{x} to be \tbx{int}. Now, if we decide to edit the function \tbx{f} so
as to relax its type,

\begin{code}
def f x y = x;                        \% *1 -> *0 -> *1
\end{code}

\hspace*{-\parindent}the type of \tbx{g} that was earlier constrained
to be {\tt (int -> int -> int)} can now also be relaxed to {\tt (*2 ->
int -> *2)}.  The system should be able to detect this as well. Note
that this relaxation does not create unsound types but may render the
original types as incomplete or non-principal.

Constraint relaxation may also occur due to a change in mutual recursion
among definitions. Consider the following example:

\begin{code}
def fst (x,y) = x;                    \% (*0,*1) -> *0
\vsp
def h x = if true then 
            x
          else fst (t x x);           \% *2 -> *2
\vsp
def t x y = h x,h y;                  \% *2 -> *2 -> (*2,*2)
\end{code}

Since \tbx{h} and \tbx{t} are mutually recursive, the type of the two arguments
of \tbx{t} are constrained to be the same. Now, if we edit the definition
for \tbx{h} to be the simple identity function,

\begin{code}
def h x = x;                          \% *2 -> *2
\end{code}

\hspace*{-\parindent}then the constraint on the arguments of \tbx{t}
is no longer present since \tbx{h} can now be instantiated
differently. Therefore, the type of \tbx{t} can be relaxed to {\tt (*3
-> *4 -> (*3,*4))}. The system should be able to detect this and flag
the recompilation of \tbx{t}.
