% -*- Mode: TeX -*-

\section{Syntax and Notation}
\label{notation}

In this section, we present a brief overview of the notation used in
this paper. Readers are referred to \cite{Gupta90,Tofte88} for
details. Those already familiar with the Hindley/Milner type system may
just skim this section for the notation --- there are no new concepts
introduced here. 

\subsection{The Expression Mini-Language}

The basic expression language used in describing the Hindley/Milner type
system is fairly small. We use the same formulation as in
\cite{Damas82,Tofte88} with only slight modifications to suit our
incremental system. The syntax of the mini-language appears
below:
\begin{eqnarray}
\label{mini-lang}
   \bx{$x,y,z$ $\in$ Identifiers} & & \\
   \bx{$c$ $\in$ Constants} & ::= & \{\tbx{true},\tbx{false},1,2,\ldots\} \\
   \bx{$e$ $\in$ Expressions} & ::= &
\begin{array}[t]{ll}
 {} & c \\
| & x \\
| & \lambda{}x.\:e_1 \\
| & e_1\;e_2 \\
| & \tbx{let $x=e_1$ in $e_2$}
\end{array} \\
\bx{$B$ $\in$ Bindings} & ::= & x = e \\
\bx{$P$ $\in$ Programs} & ::= & B_1;\;B_2;\cdots;\;B_n;\;\tbx{it}=e
\label{complete-program}
\end{eqnarray}
The above mini-language retains the notion of top-level, independent
bindings as units of compilation. A complete program is a set of such
bindings.  The final binding is special\footnote{This is adapted from
the ML interactive runtime environment where the last expression
evaluated is referred to as ``\tbx{it}''.} in that it represents a
program query and is also evaluated after being compiled within the
current environment.

We will freely (and informally) use tuple expressions and tuple
bindings in this mini-language because tuples can always be 
simulated by the function type constructor ($\rightarrow$) alone.

\subsection{The Type Language}

The standard Hindley/Milner type language is inductively defined as follows:
\begin{eqnarray}
 \bx{$\pi$ $\in$ Type-Constructors} & = & \{\ibx{int},\ibx{bool},\ldots\} \\
 \bx{$\alpha$,$\beta$ $\in$ Type-Variables} & = & \{\tbx{*0},\tbx{*1},\ldots\} \\
 \bx{$\tau$ $\in$ Types} & ::=  &
\begin{array}[t]{ll}
{} & \pi \\
| & \alpha \\
| & \tau_1\rightarrow\tau_2
\end{array} \\
 \bx{$\sigma$ $\in$ Type-Schemes} & ::= &
\begin{array}[t]{ll}
{} & \tau \\
| & \forall\alpha.\:\sigma_1 
\end{array} 
\end{eqnarray}

\subsection{Type Notation}

A {\bf Type Environment} maps identifiers to type-schemes.  All type
variables of a type $\tau$ are considered to be {\bf free} in that
type.  The quantified type-variables of a type-scheme are taken to be
{\bf bound} in that type-scheme and the other type-variables are taken
to be {\bf free}.  This definition extends pointwise to type
environments. We will denote the free type-variables of $T$ by
$\fn{tyvars}{T}$, where $T$ could either be a type, a type-scheme, or
a type environment.

A {\bf Substitution} \ibx{S} maps type-variables to types.  By
extension, we can apply substitutions to types, type-schemes, or type
environments, in each case only operating on their free type-variables.
Given a type-scheme $\sigma = \forall\alpha_1\cdots\alpha_n.\:\tau$, an
{\bf Instantiation} $\sigma\succ\tau'$ is defined by a substitution $S$ for the
bound variables of $\sigma$ so that $S\tau=\tau'$. The instantiation
$\sigma_{1}\succeq\sigma_{2}$ is valid if $\sigma_{1}\succ\tau_{2}$ (where
$\sigma_{2} = \forall\beta_1\cdots\beta_m.\:\tau_{2}$) and no $\beta_{j}$
is free in $\sigma_{1}$. The key point to remember is that substitutions
affect only free type-variables, while instantiations operate only on bound
type-variables.

Given a type $\tau$ and a type environment \ibx{TE}, we define
$\fn{close}{\ibx{TE},\tau} = \forall\alpha_1\cdots\alpha_n.\:\tau$
where $\{\alpha_1,\ldots,\alpha_n\} =
\fn{tyvars}{\tau}-\fn{tyvars}{\ibx{TE}}$. When
$\fn{tyvars}{\ibx{TE}}=\phi$, we may also write simply
$\fn{close}{\tau}$ instead of $\fn{close}{\ibx{TE},\tau}$.


