statcor.tex

\section{Static Semantics for the Core}
Our\index{20.1} first task in presenting the semantics -- whether for Core or Modules,
static or dynamic -- is to define the objects concerned. In addition
to the class of {\em syntactic} objects, which we have already defined, 
there are classes of so-called {\em semantic} objects used to describe
the meaning of the syntactic objects. Some classes contain {\em simple}
semantic objects; such objects are usually identifiers or names of some
kind. Other classes contain {\em compound} semantic objects, such as
types or environments, which are constructed from component objects.

\subsection{Simple Objects}
All semantic objects in the static semantics of the entire 
language are built from identifiers and two further kinds of simple objects: 
type constructor names and structure names.
Type constructor names are the values taken by type constructors; we shall
usually refer to them briefly as type names, but they are to be clearly
distinguished from type variables and type constructors. 
Structure names play an active role only in
the Modules semantics; they enter the Core semantics only because
they appear in structure environments, which (in turn) are needed in the Core
semantics only to determine the values of long identifiers. The simple object
classes, and the variables ranging over them, are shown in
Figure~\ref{simple-objects}. We have included $\TyVar$ in the table to
make visible the use of $\alpha$ in the semantics to range over $\TyVar$.\index{20.2}

\vspace{-7mm}
\begin{figure}[h]
\vspace{2pt}
\begin{displaymath}
\begin{array}{rclr}
\alpha\ {\rm or}\ \tyvar & \in   & \TyVar	& \mbox{type variables}\\
\t               & \in   & \TyNames	& \mbox{type names}\\
\m		& \in	& \StrNames	& \mbox{structure names}
\end{array}
\end{displaymath}
\caption{Simple Semantic Objects}
\label{simple-objects}
%\vspace{3pt}
\end{figure}

Each\index{20.3} $\alpha \in\TyVar$ possesses a boolean {\sl equality} attribute,
which determines whether or not it {\sl admits equality}, i.e. whether
it is a member of EtyVar (defined on page~\pageref{etyvar-lab}).
%-- in which case we
%also say that it is an {\sl equality} type variable. 
%poly 
Independently hereof, each $\alpha$ possesses a boolean attribute,
the {\sl imperative} attribute, which determines whether it is imperative,
i.e. whether it is a member of $\ImpTyVar$ (defined on page~\pageref{etyvar-lab})
or not.

Each $\t\in\TyNames$ has
an arity $k\geq 0$, and also possesses an equality attribute.
We denote the class of type names with arity $k$ by $\TyNamesk$.

With\index{20.35} each special constant {\scon} we associate a type
name $\scontype(\scon)$ which is either {\INT}, {\REAL} or {\STRING}
as indicated by Section~\ref{cr:speccon}.

\subsection{Compound Objects}
When\index{20.4} $A$ and $B$ are sets $\Fin A$ denotes the set of finite subsets of $A$,
and $\finfun{A}{B}$ denotes the set of {\sl finite maps} (partial functions
with finite domain) from $A$ to $B$.
The domain\index{21.1} and range of a finite map, $f$, are denoted $\Dom f$ and
$\Ran f$.
A finite map will often be written explicitly in the form $\kmap{a}{b},
\ k\geq 0$;
in particular the empty map is $\emptymap$.
We shall use the form $\{x\mapsto e\  ;\  \phi\}$ -- a form of set
comprehension -- to stand for the finite map $f$ whose domain
is the set of values $x$ which satisfy the condition $\phi$, and
whose value on this domain is given by $f(x)=e$.

When $f$ and $g$ are finite maps the map $\plusmap{f}{g}$, called
$f$ {\sl modified} by $g$, is the finite map with domain
$\Dom f \cup \Dom g$ and values
\[(\plusmap{f}{g})(a) = \mbox{if $a\in\Dom g$ then $g(a)$ else $f(a)$.}
\]

The compound objects for the static semantics of the Core Language are
shown in Figure~\ref{compound-objects}.
We take $\cup$ to mean disjoint union over
semantic object classes. We also understand all the defined object
classes to be disjoint.

\begin{figure}[h]
%\vspace{2pt}
\begin{displaymath}
\begin{array}{rcl}
        \tau	&\in	&\Type = \TyVar\cup\RecType\cup\FunType
                                 \cup\ConsType\\
 \longtauk\ {\rm or}\ \tauk
                & \in   & \Type^k\\
 \longalphak\ {\rm or}\ \alphak
                & \in   & \TyVar^k\\
 \varrho        & \in   & \RecType = \finfun{\Lab}{\Type} \\
 \tau\rightarrow\tau'
                & \in   & \FunType = \Type\times\Type \\
                &       & \ConsType = \cup_{k\geq 0}\ConsType^{(k)}\\
        \tauk\t & \in 	& \ConsType^{(k)} = \Type^k\times\TyNamesk  \\
\typefcn\ {\rm or}\ \typefcnk
        	& \in	& \TypeFcn = \cup_{k\geq 0}\TyVar^k\times\Type\\
\tych\ {\rm or}\ \longtych
        	& \in	& \TypeScheme = \cup_{k\geq 0}\TyVar^k\times\Type\\
\S\ {\rm or}\ (\m,\E)
        	& \in	& \Str = \StrNames\times\Env \\
(\theta,\CE)    & \in   & \TyStr = \TypeFcn\times\ConEnv\\
\SE		& \in	& \StrEnv = \finfun{\StrId}{\Str}\\
\TE		& \in	& \TyEnv = \finfun{\TyCon}{\TyStr}\\
\CE             & \in   & \ConEnv = \finfun{\Con}{\TypeScheme}\\
\VE		& \in	& \VarEnv = \finfun{(\Var\cup\Con\cup\Exn)}{\TypeScheme}\\
\EE		& \in	& \ExnEnv = \finfun{\Exn}{\Type}\\
\E\ {\rm or}\ \longE{}
                & \in	& \Env = \StrEnv\times\TyEnv\times\VarEnv
                                         \times\ExnEnv\\
\T              & \in   & \TyNameSets = \Fin(\TyNames)\\
\U              & \in   & \TyVarSet = \Fin(\TyVar)\\
\C\ or\ \T,\U,\E   & \in   & \Context = \TyNameSets\times\TyVarSet\times\Env
\end{array}
\end{displaymath}
\caption{Compound Semantic Objects\index{21.2}}
\label{compound-objects}
%\vspace{3pt}
\end{figure}


Note that $\Lambda$\index{21.3} and $\forall$ bind type variables.  For any semantic object
$A$, $\TyNamesFcn A$ and $\TyVarsFcn A$ denote respectively the set of
type names and the set of type variables occurring free in $A$.
Moreover, $\imptyvars A$ and $\apptyvars A$ denote respectively the set
of imperative type variables and the set of applicative
type variables occurring free in $A$.\index{21.4}
\subsection{Projection, Injection and Modification}
\label{stat-proj}\index{22.1}
{\bf Projection}: We often need to select components of tuples -- for example,
the variable-environment component of a context. In such cases we
rely on  variable names to indicate which component
is selected. For instance ``$\of{\VE}{\E}$'' means ``the variable-environment
component
of $\E$'' and ``$\of{\m}{\S}$'' means ``the structure name of $\S$''.

Moreover, when a tuple contains a finite map we shall ``apply'' the
tuple to an argument, relying on the syntactic class of the argument to
determine the relevant function. For instance $\C(\tycon)$ means
$(\of{\TE}{\C})\tycon$.

A particular case needs mention:  $\C(\con)$ is taken to stand for
$(\of{\VE}{\C})\con$; similarly, $\C(\exn)$ is taken to stand for
$(\of{\VE}{\C})\exn$.
  The type scheme of a value constructor is
held in $\VE$ as well as in $\TE$ (where it will be recorded within
a $\CE$); similarly, the type of an exception constructor is held in
$\VE$ as well as in $\EE$.
Thus the re-binding of a constructor of either kind is given proper
effect by accessing it in $\VE$, rather than in $\TE$ or in $\EE$.

Finally, environments may be applied to long identifiers.
For instance if $\longcon = \strid_1.\cdots.\strid_k.\con$ then
$\E(\longcon)$ means
\[ (\of{\VE}
       {(\of{\SE}
            {\cdots(\of{\SE}
                       {(\of{\SE}{\E})\strid_1}
                   )\strid_2\cdots}
        )\strid_k}
    )\con.
\]

{\bf Injection}: Components may be injected into tuple classes; for example,\linebreak
``$\VE\ \In\ \Env$'' means the environment
$(\emptymap,\emptymap,\VE,\emptymap)$.

{\bf Modification}: The modification of one map $f$ by another map $g$,
written $f+g$, has already been mentioned.  It is commonly used for
environment modification, for example $\E+\E'$.  Often, empty components
will be left implicit in a modification; for example $\E+\VE$ means
$\E+(\emptymap,\emptymap,\VE,\emptymap)$.  For set components, modification
means union, so that $\C+(\T,\VE)$ means
\[ (\ (\of{\T}{\C})\cup\T,\ \of{\U}{\C},\ (\of{\E}{\C})+\VE\ ) \]
Finally, we frequently need to modify a context $\C$ by an environment $\E$
(or a type environment $\TE$ say),
at the same time extending $\of{\T}{\C}$ to include the type names of $\E$
(or of $\TE$ say).
We therefore define $\C\oplus\TE$,\index{22.2} for example, to mean
$\C+(\TyNamesFcn\TE,\TE)$.

\subsection{Types and Type functions}
\label{tyfun-sec}
A type $\tau$ is an {\sl equality type},\index{22.3} or {\sl admits equality}, if it is
of one of the forms
\begin{itemize}
\item $\alpha$, where $\alpha$ admits equality;
\item $\{\lab_1\mapsto\tau_1,\ \cdots,\ \lab_n\mapsto\tau_n\}$,
      where each $\tau_i$ admits equality;
\item $\tauk\t$, where $t$ and all members of $\tauk$ admit equality;
\item $(\tau')\REF$.\index{23.1}
\end{itemize}
\label{tyfcn-lab}
A type function $\theta=\Lambda\alphak.\tau$\index{23.2}
 has arity $k$; it must be
{\sl closed} -- i.e.
$\TyVarFcn(\tau)\subseteq\alphak$ -- and the bound variables must
be distinct. Two type functions are considered equal
if they only differ in their choice of bound variables (alpha-conversion).
In particular, the equality attribute has no significance in a 
bound variable of a type function; for example, $\Lambda\alpha.\alpha\to
\alpha$ and $\Lambda\beta.\beta\to\beta$ are equal type functions
even if $\alpha$ admits equality but $\beta$ does not.
%poly 
Similarly, the imperative attribute has no significance 
in the bound variable of a type function.
If $t$ has arity $k$, then we write $t$ to mean $\Lambda\alphak.\alphak\t$
(eta-conversion); thus $\TyNames\subseteq\TypeFcn$. $\theta=\Lambda\alphak.\tau$
is an {\sl equality} type function, or {\sl admits equality}, if when the
type variables $\alphak$ are chosen to admit equality then $\tau$ also admits
equality.

We write the application of a type function $\theta$ to a vector
$\tauk$ of types as $\tauk\theta$.
If $\theta=\Lambda\alphak.\tau$ we set $\tauk\theta=\tau\{\tauk/\alphak\}$
(beta-conversion). 

We write $\tau\{\thetak/\tk\}$ for the result of substituting type
functions $\thetak$ for type names $\tk$ in $\tau$.
We assume that all beta-conversions
are carried out after substitution, so that for example
\[(\tauk\t)\{\Lambda\alphak.\tau/\t\}=\tau\{\tauk/\alphak\}.\]
%poly 
\label{imp-ty-lab}
A type is {\sl imperative} if all type variables occurring in it are
imperative.
\subsection{Type Schemes}
\label{type-scheme-sec}
A type scheme $\tych=\forall\alphak.\tau$\index{23.3}
 {\sl generalises} a type $\tau'$,
written $\tych \succ\tau'$,
if $\tau'=\tau\{\tauk/\alphak\}$ for some $\tauk$, where each member $\tau_i$
of $\tauk$ admits equality if $\alpha_i$ does,  
%poly 
and $\tau_i$ is imperative if $\alpha_i$ is imperative.
If $\tych'=\forall\beta^{(l)}.\tau'$ then $\tych$ {\sl generalises} $\tych'$,
written $\tych\succ\tych'$, if $\tych\succ\tau'$ and $\beta^{(l)}$ contains
no free type variable of $\tych$.
It can be shown that $\tych\succ\tych'$ iff, for all $\tau''$, whenever
$\tych'\succ\tau''$ then also $\tych\succ\tau''$.

Two type schemes $\tych$ and $\tych'$ are considered equal
if they can be obtained from each other by
renaming and reordering of bound type variables, and deleting type
variables from the prefix which do not occur in the body.
Here, in contrast to the case for type functions, the equality attribute
must be preserved in renaming; for example $\forall\alpha.\alpha\to\alpha$
and $\forall\beta.\beta\to\beta$ are only equal if either both $\alpha$
and $\beta$ admit equality, or neither does.
%poly 
Similarly, the imperative attribute of a bound type variable of a
type scheme {\sl is} significant.
It can be shown that $\tych=\tych'$ iff $\tych\succ\tych'$ and
$\tych'\succ\tych$.

We consider a type $\tau$ to be a type scheme, identifying it with
$\forall().\tau$.

\subsection{Scope of Explicit Type Variables}
\label{scope-sec}

In\index{23.10} the Core language, a type or datatype binding can 
explicitly introduce type variables whose scope is that binding.
In the modules, a description of a value, type, or datatype
may contain explicit type variables whose scope is that
description. However, we\index{23.11} still have to account for the
scope of an explicit type variable occurring in the ``\ml{:} $\ty$'' 
of a typed expression or pattern 
or in the ``\ml{of} $\ty$'' of an exception binding. For the rest
of this section, we consider such occurrences of type variables only.

Every occurrence of a value declaration is said to
{\sl scope} a set of explicit type variables determined as follows.



%Every explicit type variable $\alpha$ is {\sl scoped at} a value binding
%which is determined as follows.

First, an occurrence of $\alpha$ in a value declaration $\valdec$ is said
to be {\sl unguarded} if the occurrence is not part of a smaller value
declaration within $\valbind$.
In this case we say that $\alpha$ {\sl occurs unguarded} in the 
value declaration.

Then we say that $\alpha$ is {\sl scoped at} a particular occurrence
$O$ of $\valdec$ in a program if 
(1) $\alpha$ occurs unguarded in this value declaration, and 
(2) $\alpha$ does not occur unguarded in any larger value declaration
containing the occurrence $O$.\label{scope-def-lab}

Hence, associated with every occurrence of a value declaration there is 
a set $\U$ of the explicit type variables that are scoped at that
occurrence. One may think of each occurrence of $\VAL$ as being implicitly
decorated with such a  set, for instance:

\vspace*{3mm}
\halign{\indent$#$&$#$&$#$\cr
\mbox{$\VAL_{\{\}}$ \ml{x = }}&\mbox{\ml{(}}&
\mbox{\ml{let $\VAL_{\{\mbox{\ml{'a}}\}}$ Id1:'a->'a = fn z=>z in Id1 Id1 end,}}\cr
& &\mbox{\ml{let $\VAL_{\{\mbox{\ml{'a}}\}}$ Id2:'a->'a = fn z=>z in Id2 Id2 end)}}\cr
\noalign{\vspace*{3mm}}
\mbox{$\VAL_{\{\mbox{\ml{'a}}\}}$ \ml{x = }}&\mbox{\ml{(}}&
\mbox{\ml{let $\VAL_{\{\}}$ Id:'a->'a = fn z=>z in Id Id end,}}\cr
& &\mbox{\ml{fn z=> z:'a)}}\cr}

According to the inference rules in Section~\ref{stat-cor-inf-rules}
the first example can be elaborated, but the second cannot since \ml{'a}
is bound at the outer value declaration leaving no possibility of two 
different instantiations of the type of \ml{Id} in the application
\ml{Id Id}.



\subsection{Non-expansive Expressions}
\label{expansive-sec}
In\index{23.4} order to treat polymorphic references and exceptions,
the set Exp of expressions is partitioned into two classes, the {\sl
expansive} and the {\sl non-expansive} expressions. Any variable,
constructor and $\FN$ expression, possibly constrained by one or more
type expressions, is non-expansive; all other expressions are said to
be expansive.  The idea is that the dynamic evaluation of a
non-expansive expression will neither generate an exception nor extend
the domain of the memory, while the evaluation of an expansive
expression might.

\subsection{Closure}
\label{closure-sec}
Let\index{24.2} $\tau$ be a type and $A$ a semantic object. Then $\cl{A}{(\tau)}$,
the {\sl closure} of $\tau$ with respect to $A$, is the type scheme
$\forall\alphak.\tau$, where $\alphak=\TyVarFcn(\tau)\setminus\TyVarFcn A$.
Commonly, $A$ will be a context $\C$.
We abbreviate the {\sl total} closure $\cl{\emptymap}{(\tau)}$ to
$\cl{}{(\tau)}$.
If the range of a variable environment $\VE$ contains only types (rather than
arbitrary type schemes) we set
\[\cl{A}{\VE}=\{\id\mapsto\cl{A}{(\tau)}\ ;\ \VE(\id)=\tau\}\]
with a similar definition for $\cl{A}{\CE}$.

\label{clos-def-lab}
Closing\index{24.3} a variable environment $\VE$ that stems from
the elaboration of a value binding $\valbind$ requires extra
care to ensure type security of references and exceptions and correct
scoping of explicit type variables.
Recall that $\valbind$ is not allowed to bind the
same variable twice. Thus, for each $\var\in\Dom\VE$ 
there is a unique \mbox{\pat\ \ml{=} \exp}
in $\valbind$ which binds $\var$. 
If $\VE(\var)=\tau$, let 
$\cl{\C,\valbind}{\VE(\var)}=\longtych$, where
\[\alphak=\cases{\TyVarFcn\tau\setminus\TyVarFcn\C,&if $\exp$ 
                                                    is non-expansive;\cr
                 \apptyvars\tau\setminus\TyVarFcn\C,&if $\exp$ is expansive.}
\]
%(Explicit type variables necessitate a slight strengthening of the requirements
%which a type variable must satisfy in order to be bound: a type variable 
%occurring unguarded in $\valbind$ can be admitted among $\alphak$ only
%if it is scoped at the particular occurrence of $\valbind$ at which
%the closure operation is performed.)

Notice that the form of $\valbind$ does not affect the binding of
applicative type variables, only the binding of imperative
type variables.

\subsection{Type Structures and Type Environments}
\label{typeenv-wf-sec}
A type\index{24.4} structure $(\theta,\CE)$ is {\sl well-formed} if either
$\CE=\emptymap$, or $\theta$ is a type name $t$.
(The latter case arises, with $\CE\neq\emptymap$, in $\DATATYPE$
declarations.)
All type structures occurring in elaborations are assumed to
be well-formed.

A type structure $(\t,\CE)$ is said to
{\sl respect equality} if, whenever $\t$ admits equality, then
either $\t=\REF$ (see Appendix~\ref{init-stat-bas-app}) or,
for each $\CE(\con)$ of the form 
$\forall\alphak.(\tau\rightarrow\alphak\t)$,
the type function $\Lambda\alphak.\tau$ also admits equality.
(This ensures that the equality
predicate ~{\tt =}~ will be applicable to a constructed value $(\con,v)$ of
type $\tauk\t$ only when it is applicable to the value $v$ itself,
whose type is $\tau\{\tauk/\alphak\}$.)
A type environment $\TE$ {\sl respects equality} if all its type
structures do so.

Let $\TE$ be a type environment, and let $T$ be the set of type names
$\t$ such that $(\t,\CE)$ occurs in $\TE$ for some
$\CE\neq\emptymap$.  Then $\TE$ is said to {\sl maximise equality}
if (a) $\TE$ respects equality, and also (b) if any larger subset of
$T$ were to admit equality (without any change in the equality
attribute of any type names not in $T$) then $\TE$ would cease to
respect equality.


For any $\TE$ of the form
\[\TE=\{\tycon_i\mapsto(t_i,\CE_i)\ ;\ 1\leq i\leq k\},\]
where no $\CE_i$ is the empty map, and for any $\E$ we define
$\Abs(\TE,\E)$ to\index{25.1} be the environment obtained from 
$\E$ and $\TE$ as
follows. First, let $\Abs(\TE)$ be the type environment
$\{\tycon_i\mapsto(t_i,\emptymap)\ ;\ 1\leq i\leq k\}$
in which all constructor
environments $\CE_i$ have been replaced by the empty map. 
Let $t_1',\cdots,t_k'$ be new distinct type names none of which
admit equality. Then $\Abs(\TE,\E)$ is the result of simultaneously
substituting
$t_i'$ for $t_i$, $1\leq i\leq k$,  throughout $\Abs(\TE)+\E$. 
(The effect of the latter substitution is to ensure that the use of 
equality on  an $\ABSTYPE$ is restricted to the $\WITH$ part.)
\label{abs-lab}
\clearpage

\subsection{Inference Rules}
\label{stat-cor-inf-rules}
Each rule\index{26.1} of the semantics allows inferences among sentences of the form
\[A\ts{\it phrase}\ra A'\]
where
$A$ is usually an environment or a context, {\it phrase} is a phrase of
the Core, and $A'$ is a semantic object -- usually a type or an
environment.  It may be pronounced ``{\it phrase} elaborates to $A'$ in
(context or environment) $A$''.  Some rules have extra hypotheses not of
this form; they are called {\sl side conditions}.  

In the presentation of the rules, phrases within single
angle brackets ~$\langle\ \rangle$~ are called {\sl
first options}, and those within double
angle brackets ~$\langle\langle\ \rangle\rangle$~ are called {\sl
second options}.  To reduce the number of rules, we have adopted the
following convention:
\begin{quote} In each instance of a rule, the
first options must be either all present or all absent;
similarly the second options must be either all present or all absent.
\end{quote}

Although not assumed in our definitions, it is intended that every
context $\C=\T,\U,\E$ has the property that $\TyNamesFcn\E\subseteq\T$.
Thus $\T$ may be thought of, loosely, as containing all type names
which ``have been generated''. It is necessary to include $\T$ as a
separate component in a context, since $\TyNamesFcn\E$ may not contain
all the type names which have been generated; one reason is that a
context $\T,\emptyset,\E$ is a projection of the basis
$\B=(\M,\T),\F,\G,\E$ whose other components $\F$ and $\G$
could contain other such names -- recorded in $\T$ but not present in
$\E$.  Of course, remarks about what ``has been generated'' are not
precise in terms of the semantic rules. But the following precise result
may easily be demonstrated:
\begin{quote}
Let S be a sentence
~$\T,\U,\E\ts{\it phrase}\ra A$~ such that
$\TyNamesFcn\E\subseteq\T$,
and let S$'$ be a sentence
~$\T',\U',\E'\ts{\it phrase}'\ra A'$~
occurring in a proof of S; then also
$\TyNamesFcn\E'\subseteq\T'$.
\end{quote}



%                       Atomic Expressions
%
\rulesec{Atomic Expressions\index{26.2}}{\C\vdash\atexp\ra\tau}
%\begin{figure}[h]

\begin{equation}	% special constant
\label{sconexp-rule}
\frac{}
     {\C\ts\scon\ra\scontype(\scon)}\index{26.3}
\end{equation}

\begin{equation}	% value variable
\label{varexp-rule}
\frac{\C(\longvar)\succ\tau}
     {\C\ts\longvar\ra\tau}
\end{equation}

\begin{equation}	% value constructor
\label{conexp-rule}
\frac{\C(\longcon)\succ\tau}
     {\C\ts\longcon\ra\tau}
\end{equation}

\begin{equation}      % exception constant
%\label{exconexp-rule}
\frac{\C(\longexn)=\tau}
     {\C\ts\longexn\ra\tau}
\end{equation}

\begin{equation}	% record expression
%\label{recexp-rule}
\frac{\langle\C\ts\labexps\ra\varrho\rangle}
     {\C\ts\ttlbrace\ \recexp\ \ttrbrace\ra\emptymap\langle +\ \varrho\rangle{\rm\ in\ \Type}}\index{27.0}
\end{equation}

\begin{equation}        % local declaration
\label{let-rule}
\frac{\C\ts\dec\ra\E\qquad\C\oplus\E\ts\exp\ra\tau}
     {\C\ts\letexp\ra\tau}\index{27.1}
\end{equation}

\begin{equation}	% paren expression
%\label{parexp-rule}
\frac{\C\ts\exp\ra\tau}
     {\C\ts\parexp\ra\tau}
\end{equation}
\comments
\begin{description}
\item{(\ref{varexp-rule}),(\ref{conexp-rule})} 
The instantiation of 
type schemes allows different occurrences of a single $\longvar$ 
or $\longcon$ to assume different types.
\item{(\ref{let-rule})} 
The use of $\oplus$, here and elsewhere, ensures that
type names generated by the first sub-phrase are different from 
type names generated by the second sub-phrase.
\end{description}

\rulesec{Expression Rows}{\C\ts\labexps\ra\varrho}
\begin{equation}	% expression rows
%\label{labexps-rule}
\frac{\C\ts\exp\ra\tau\qquad\langle\C\ts\labexps\ra\varrho\rangle}
     {\C\ts\longlabexps\ra\{\lab\mapsto\tau\}\langle +\ \varrho\rangle}\index{27.2}
\end{equation}
%                        Expressions
%
\rulesec{Expressions}{\C\ts\exp\ra\tau}
%\vspace{6pt}
%\fbox{$\C\ts\exp\ra\tau$}
\begin{equation}	% atomic
\label{atexp-rule}
\frac{\C\ts\atexp\ra\tau}
     {\C\ts\atexp\ra\tau}\index{27.3}
\end{equation}

\begin{equation}	% application
%\label{app-rule}
\frac{\C\ts\exp\ra\tau'\rightarrow\tau\qquad\C\ts\atexp\ra\tau'}
     {\C\ts\appexp\ra\tau}
\end{equation}

\begin{equation}	% typed
\label{typedexp-rule}
\frac{\C\ts\exp\ra\tau\qquad\C\ts\ty\ra\tau}
     {\C\ts\typedexp\ra\tau}
\end{equation}

\begin{equation}        % handle exception
%\label{handlexp-rule}
\frac{\C\ts\exp\ra\tau\qquad\C\ts\match\ra\EXCN\rightarrow\tau}
     {\C\ts\handlexp\ra\tau}
\end{equation}

\begin{equation}        % raise exception
\label{raiseexp-rule}
\frac{\C\ts\exp\ra\EXCN}
     {\C\ts\raisexp\ra\tau}
\end{equation}

\begin{equation}        % function
%\label{fnexp-rule}
\frac{\C\ts\match\ra\tau}
     {\C\ts\fnexp\ra\tau}
\end{equation}
\comments
\begin{description}
\item{(\ref{atexp-rule})}
The relational symbol $\ts$ is overloaded for all syntactic classes (here
atomic expressions and expressions).
\item{(\ref{typedexp-rule})}
Here $\tau$ is determined by $\C$ and $\ty$. Notice that type variables
in $\ty$ cannot be instantiated in obtaining $\tau$; thus the expression
\verb+1:'a+ will not elaborate successfully, nor will the expression
\verb+(fn x=>x):'a->'b+.
The effect of type variables in an explicitly typed expression is
to indicate exactly the degree of polymorphism present in the expression.\index{27.4}
\item{(\ref{raiseexp-rule})}
Note that $\tau$ does not occur in the premise; thus a $\RAISE$
expression has ``arbitrary'' type.
\end{description}
%                        Matches 
%
\rulesec{Matches}{\C\ts\match\ra\tau}
\begin{equation}	% match
%\label{match-rule}
\frac{\C\ts\mrule\ra\tau\qquad\langle\C\ts\match\ra\tau\rangle}
     {\C\ts\longmatch\ra\tau}\index{28.1}
\end{equation}
\rulesec{Match Rules}{\C\ts\mrule\ra\tau}
\begin{equation}	% mrule
%\label{mrule-rule}
\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C+\VE\ts\exp\ra\tau'}
     {\C\ts\longmrule\ \ra\tau\rightarrow\tau'}
\end{equation}
\comment  This rule allows new free type variables to enter
the context. These new type variables will be chosen, in effect, during
the elaboration of $\pat$ (i.e., in the inference of the first
hypothesis). In particular, their choice may have to be made to
agree with type variables present in any explicit type expression
occurring within $\exp$ (see rule~\ref{typedexp-rule}).

%
%                        Declarations
%
\rulesec{Declarations}{\C\ts\dec\ra\E}
%poly
\begin{equation}	% value declaration
\label{valdec-rule}
\frac{\plusmap{\C}{\U}\ts\valbind\ra\VE\qquad 
      \VE'=\cl{\C,\valbind}{\VE}\qquad
      \U\cap\TyVarFcn\VE'=\emptyset}
     {\C\ts\valdecS\ra\VE'\ \In\ \Env}\index{28.2}
\end{equation}
%from version 1, without polymorphic refs:
%\begin{equation}	% value declaration
%\label{valdec-rule}
%\frac{\C\ts\valbind\ra\VE}
%     {\C\ts\valdec\ra\cl{\C}{\VE}\ \In\ \Env}
%\end{equation}

\begin{equation}	% type declaration
%\label{typedec-rule}
\frac{\C\ts\typbind\ra\TE}
     {\C\ts\typedec\ra\TE\ \In\ \Env}
\end{equation}

\begin{equation}	% datatype declaration
\label{datatypedec-rule}
\frac{\begin{array}{c}
\C\oplus\TE\ts\datbind\ra\VE,\TE\qquad
      \forall(\t,\CE)\in\Ran\TE,\ \t\notin(\of{\T}{\C}) \\
     \mbox{$\TE$ maximises equality}
     \end{array}
     }
     {\C\ts\datatypedec\ra(\VE,\TE)\ \In\ \Env}
\end{equation}

\begin{equation}	% abstype declaration
\label{abstypedec-rule}
\frac{\begin{array}{rl}
      \C\oplus\TE\ts\datbind\ra\VE,\TE\qquad &
      \forall(\t,\CE)\in\Ran\TE,\ \t\notin(\of{\T}{\C})\\
      \C\oplus(\VE,\TE)\ts\dec\ra\E\qquad & 
     \mbox{$\TE$ maximises equality}
      \end{array}
     }
     {\C\ts\abstypedec\ra\Abs(\TE,\E)}
\end{equation}

\begin{equation}	% exception declaration
\label{exceptiondec-rule}
\frac{\C\ts\exnbind\ra\EE\quad\VE=\EE }
     {\C\ts\exceptiondec\ra(\VE,\EE)\ \In\ \Env }
\end{equation}

\begin{equation}	% local declaration
%\label{localdec-rule}
\frac{\C\ts\dec_1\ra\E_1\qquad\C\oplus\E_1\ts\dec_2\ra\E_2}
     {\C\ts\localdec\ra\E_2}\index{28.3}
\end{equation}

\begin{equation}                % open declaration
%\label{open-dec-rule}
\frac{ \C(\longstrid_1)=(\m_1,\E_1)
            \quad\cdots\quad
       \C(\longstrid_n)=(\m_n,\E_n) }
     { \C\ts\openstrdec\ra \E_1 + \cdots + \E_n }
\end{equation}

\begin{equation}	% empty declaration
%\label{emptydec-rule}
\frac{}
     {\C\ts\emptydec\ra\emptymap\ \In\ \Env}
\end{equation}

\begin{equation}	% sequential declaration
%\label{seqdec-rule}
\frac{\C\ts\dec_1\ra\E_1\qquad\C\oplus\E_1\ts\dec_2\ra\E_2}
     {\C\ts\seqdec\ra\plusmap{E_1}{E_2}}
\end{equation}
\comments
\begin{description}
\item{(\ref{valdec-rule})}
Here $\VE$ will contain types rather than general
type schemes. The closure of $\VE$ is exactly what allows variables to
be used polymorphically, via rule~\ref{varexp-rule}.

Moreover, $\U$ is the set of explicit type variables scoped at this particular
occurrence of $\valdec$, cf. Section~\ref{scope-sec}, 
page~\pageref{scope-def-lab}. The side-condition on $\U$
ensures that these explicit type variables are bound by the closure operation.
On the other hand, no {\sl other} explicit type variable occurring
free in $\VE$ will become bound, since it must be in $\of{\U}{\C}$, and
is therefore excluded from closure by the definition of the closure operation
(Section~\ref{closure-sec}, page~\pageref{clos-def-lab})
since $\of{\U}{\C}\subseteq\TyVarFcn\C$.
\item{(\ref{datatypedec-rule}),(\ref{abstypedec-rule})}
The side conditions
express that the elaboration of each datatype binding
generates new type names and that as many of these new names
as possible admit equality.  Adding $\TE$ to the context on the left
of the $\ts$ captures the recursive nature of the binding.
%The side condition is
%the formal way of expressing that the elaboration of each datatype binding
%generates new type names.  Adding $\TE$ to the context on the left
%of the $\ts$ captures the recursive nature of the binding. Recall that $\TE$
%is assumed well-formed (as defined in Section~\ref{typeenv-wf-sec}). If
%$\TyNamesFcn(\of{\E}{\C})\subseteq\of{\T}{\C}$ and the side condition is
%satisfied then $\C\oplus\TE$ is well-formed.
\item{(\ref{abstypedec-rule})}
The $\Abs$ operation was defined in Section~\ref{typeenv-wf-sec}, page~\pageref{abs-lab}.
\item{(\ref{exceptiondec-rule})}
No closure operation is used here, since $\EE$ maps exception 
names to types rather than  to general type schemes.
Note that $\EE$ is also recorded in the {\VarEnv} component of
the resulting environment (see Section~\ref{stat-proj}, page~\pageref{stat-proj}).\index{29.0}
\end{description}

%                        Bindings
%
\rulesec{Value Bindings}{\C\ts\valbind\ra\VE}
%\vspace{6pt}
\begin{equation}	% value binding
\label{valbind-rule}
\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C\ts\exp\ra\tau\qquad
      \langle\C\ts\valbind\ra\VE'\rangle }
     {\C\ts\longvalbind\ra\VE\ \langle +\ \VE'\rangle}\index{29.1}
\end{equation}

\begin{equation}	% recursive value binding
\label{recvalbind-rule}
\frac{\C+\VE\ts\valbind\ra\VE}
     {\C\ts\recvalbind\ra\VE}
\end{equation}
\comments
\begin{description}
\item{(\ref{valbind-rule})}
When the option is present we have $\Dom\VE\cap
\Dom\VE' = \emptyset$ by the syntactic restrictions.\index{29.2}
\item{(\ref{recvalbind-rule})}
Modifying $\C$ by $\VE$ on the left captures the 
recursive nature of the binding. From rule~\ref{valbind-rule} we see that any
type scheme occurring in $\VE$ will have to be a type. Thus each use of a
recursive function in its own body must be ascribed the same type.
\end{description}

\rulesec{Type Bindings}{\C\ts\typbind\ra\TE}
%\fbox{$\C\ts\typbind\ra\TE$}
\begin{equation}	% type binding
%\label{typbind-rule}
\frac{\tyvarseq=\alphak\qquad\C\ts\ty\ra\tau\qquad
      \langle\C\ts\typbind\ra\TE\rangle}
     {\begin{array}{c}
      \C\ts\longtypbind\ra\\
      \qquad\qquad\qquad
      \{\tycon\mapsto(\typefcnk,\emptymap)\}\ \langle +\ \TE\rangle
      \end{array}
     }\index{29.3}
\end{equation}
\comment The syntactic restrictions ensure that the type function
$\typefcnk$ satisfies the well-formedness constraints of 
Section~\ref{tyfun-sec} and they ensure $tycon\notin\Dom\TE$.

\rulesec{Data Type Bindings}{\C\ts\datbind\ra\VE,\TE}
%\fbox{$\C\ts\datbind\ra\VE,\TE$}
\begin{equation}	% datatype binding
%\label{datbind-rule}
\frac{\begin{array}{c}
        \tyvarseq=\alphak\qquad\C,\alphakt\ts\constrs\ra\CE\\
        \langle\C\ts\datbind\ra\VE,\TE\qquad
        \forall(\t',\CE)\in\Ran\TE, \t\neq\t'\rangle
      \end{array}
     }
     {\begin{array}{c}
        \C\ts\longdatbind\ra\\
        \qquad\qquad\qquad\cl{}{\CE}\langle +\ \VE\rangle,\
        \{\tycon\mapsto(\t,\cl{}{\CE})\}\ \langle +\ \TE\rangle
      \end{array}
     }\index{30.1}
\end{equation}
\comment The syntactic restrictions ensure $\Dom\VE\cap\Dom\CE = \emptyset$
and $\tycon\notin\Dom\TE$.

\rulesec{Constructor Bindings}{\C,\tau\ts\constrs\ra\CE}
%\fbox{$\C,\tau\ts\constrs\ra\CE$}
\begin{equation}	% data constructors
%\label{constrs-rule}
\frac{\langle\C\ts\ty\ra\tau'\rangle\qquad
      \langle\langle\C,\tau\ts\constrs\ra\CE\rangle\rangle }
     {\begin{array}{c}
      \C,\tau\ts\longerconstrs\ra\\
      \qquad\qquad\qquad\{\con\mapsto\tau\}\
     \langle +\ \{\con\mapsto\tau'\to\tau\}\ \rangle\
      \langle\langle +\ \CE\rangle\rangle
      \end{array}
     }\index{30.2}
\end{equation}
\comment By the syntactic restrictions $\con\notin\Dom\CE$.

\rulesec{Exception Bindings}{\C\ts\exnbind\ra\EE}
%poly with polymorphic exceptions:
\begin{equation}	% exception binding
\label{exnbind1-rule}
\frac{\langle\C\ts\ty\ra\tau\quad\mbox{$\tau$ is imperative}\rangle\qquad
      \langle\langle\C\ts\exnbind\ra\EE\rangle\rangle }
     {\begin{array}{c}
      \C\ts\longexnbinda\ra\\
      \qquad\qquad\qquad\{\exn\mapsto\EXCN\}\
      \langle +\ \{\exn\mapsto\tau\rightarrow\EXCN\}\ \rangle\
      \langle\langle +\ \EE\rangle\rangle
      \end{array}
     }\index{30.3}
\end{equation}

%with mono typed exceptions:
%\begin{equation}	% exception binding
%\label{exnbind1-rule}
%\frac{\langle\C\ts\ty\ra\tau\quad\TyVarFcn(\tau)=\emptyset\rangle\qquad
%      \langle\langle\C\ts\exnbind\ra\EE\rangle\rangle }
%     {\begin{array}{c}
%      \C\ts\longexnbinda\ra\\
%      \qquad\qquad\qquad\{\exn\mapsto\EXCN\}\
%      \langle +\ \{\exn\mapsto\tau\rightarrow\EXCN\}\ \rangle\
%      \langle\langle +\ \EE\rangle\rangle
%      \end{array}
%     }
%\end{equation}

\vspace*{4mm}
\begin{equation}	% exception binding
\label{exnbind2-rule}
\frac{\C(\longexn)=\tau\qquad
      \langle\C\ts\exnbind\ra\EE\rangle }
      {\C\ts\longexnbindb\ra\{\exn\mapsto\tau\}\ \langle +\ \EE\rangle}
%     {\begin{array}{c}
%      \C\ts\longexnbindb\ra\\
%      \qquad\qquad\qquad\{\exn\mapsto\tau\}\
%      \langle +\ \EE\rangle
%      \end{array}
%     }
\end{equation}
\comments
\begin{description}
\item{(\ref{exnbind1-rule})} Notice that $\tau$ must not contain
any applicative type variables.\index{30.35}
%with monotyped exceptions:
%\item{(\ref{exnbind1-rule})} Notice that $\tau$ must be a monotype
%(see also restriction~\ref{monotypes-res} in 
%Section~\ref{further-restrictions-sec}).
\item{(\ref{exnbind1-rule}),(\ref{exnbind2-rule})}
There is a unique $\EE$, for each $\C$ and $\exnbind$,
%No matter which of the options are present, given $\C$ and $\exnbind$ there
%is at most one $\EE$ 
such that $\C\ts\exnbind\ra\EE$.
\end{description}

%\caption{Rules for Bindings}
%\end{figure}

%                        Atomic Patterns
%
\rulesec{Atomic Patterns}{\C\ts\atpat\ra(\VE,\tau)}
%\vspace{6pt}
%\fbox{$\C\ts\atpat\ra(\VE,\tau)$}
\begin{equation}	% wildcard pattern
%\label{wildcard-rule}
\frac{}
     {\C\ts\wildpat\ra (\emptymap,\tau)}\index{30.4}
\end{equation}

\begin{equation}	% special constant in pattern
\frac{}
     {\C\ts\scon\ra (\emptymap,\scontype(\scon))}\index{30.5}
\end{equation}

\begin{equation}	% variable pattern
\label{varpat-rule}
\frac{}
     {\C\ts\var\ra (\{\var\mapsto\tau\},\tau) }
\end{equation}

\begin{equation}	% constant pattern
%\label{constpat-rule}
\frac{\C(\longcon)\succ\tauk\t }
     {\C\ts\longcon\ra (\emptymap,\tauk\t)}
\end{equation}

\begin{equation}       % exception constant
%\label{exconapat-rule}
\frac{\C(\longexn)=\EXCN}
     {\C\ts\longexn\ra (\emptymap,\EXCN)}
\end{equation}



\begin{equation}	% record pattern
%\label{recpat-rule}
\frac{\langle\C\ts\labpats\ra(\VE,\varrho)\rangle}
     {\C\ts\lttbrace\ \recpat\ \rttbrace\ra(\ \emptymap\langle +\ \VE\rangle,\ \emptymap
      \langle +\ \varrho\rangle\ \In\ \Type\ ) }\index{31.1}
\end{equation}

\begin{equation}	% parenthesised pattern
%\label{parpat-rule}
\frac{\C\ts\pat\ra(\VE,\tau)}
     {\C\ts\parpat\ra(\VE,\tau)}
\end{equation}
\comments
\begin{description}
\item{(\ref{varpat-rule})} 
Note that $\var$ can assume a type, not a general type scheme.
\end{description}

\rulesec{Pattern Rows}{\C\ts\labpats\ra(\VE,\varrho)}
%\fbox{$\C\ts\labpats\ra(\VE,\varrho)$}
\begin{equation}	% wildcard record
%\label{wildrec-rule}
\frac{}
     {\C\ts\wildrec\ra(\emptymap,\varrho)}\index{31.2}
\end{equation}

\begin{equation}	% record component
\label{longlab-rule}
\frac{\C\ts\pat\ra(\VE,\tau)\qquad
      \langle\C\ts\labpats\ra(\VE',\varrho)\qquad\lab\notin\Dom\varrho\rangle
}
     {\C\ts\longlabpats\ra
     (\VE\langle +\ \VE'\rangle,\
      \{\lab\mapsto\tau\}\langle +\ \varrho\rangle) }
\end{equation}
\comment 
\begin{description}
\item{(\ref{longlab-rule})} 
 By the syntactic restrictions, $\Dom\VE\cap\Dom\VE' = \emptyset$.
\end{description}
%                        Patterns
%
%\begin{figure}[h]
%\label{pat-rules}
\rulesec{Patterns}{\C\ts\pat\ra(\VE,\tau)}
\begin{equation}	% atomic pattern
%\label{atpat-rule}
\frac{\C\ts\atpat\ra (\VE,\tau)}
     {\C\ts\atpat\ra (\VE,\tau)}\index{31.3}
\end{equation}

\begin{equation}	% construction pattern
%\label{conpat-rule}
\frac{\C(\longcon)\succ\tau'\to\tau\qquad\C\ts\atpat\ra(\VE,\tau')}
     {\C\ts\conpat\ra (\VE,\tau)}
\end{equation}

\begin{equation}       %  exception construction pattern
%\label{exconpat-rule}
\frac{\C(\longexn)=\tau\rightarrow\EXCN\qquad
      \C\ts\atpat\ra(\VE,\tau)}
     {\C\ts\exconpat\ra(\VE,\EXCN)}
\end{equation}

\begin{equation}	% typed pattern
%\label{typedpat-rule}
\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C\ts\ty\ra\tau}
     {\C\ts\typedpat\ra (\VE,\tau)}
\end{equation}

\begin{equation}	% layered pattern
\label{layeredpat-rule}
\frac{\begin{array}{c}
      \C\ts\var\ra(\VE,\tau)\qquad\langle\C\ts\ty\ra\tau\rangle\\
      \C\ts\pat\ra(\VE',\tau)
%\qquad\VE\sim\VE'
      \end{array}
     }
     {\C\ts\layeredpat\ra(\plusmap{\VE}{\VE'},\tau)}
\end{equation}
\comments
\begin{description}
\item{(\ref{layeredpat-rule})}
By the syntactic restrictions, $\Dom\VE\cap\Dom\VE' = \emptyset$.
\end{description}


%                        Type Expressions
\rulesec{Type Expressions}{\C\ts\ty\ra\tau}
\begin{equation}	% atype variable
%\label{tyvar-rule}
\frac{\tyvar=\alpha}
     {\C\ts\tyvar\ra\alpha}\index{32.1}
\end{equation}

\begin{equation}	% record type
%\label{rectype-rule}
\frac{\langle\C\ts\labtys\ra\varrho\rangle}
     {\C\ts\lttbrace\ \rectype\ \rttbrace\ra\emptymap\langle +\ \varrho\rangle\ \In\ \Type}
\end{equation}

\begin{equation}	% constructed type
\label{constype-rule}
\frac{\begin{array}{c}
      \tyseq=\ty_1\cdots\ty_k\qquad\C\ts\ty_i\ra\tau_i\ (1\leq i\leq k)\\
      \C(\longtycon)=(\theta,\CE)
      \end{array}
     }
     {\C\ts\constype\ra\tauk\theta}
\end{equation}

\begin{equation}	% function type
%\label{funtype-rule}
\frac{\C\ts\ty\ra\tau\qquad\C\ts\ty'\ra\tau'}
     {\C\ts\funtype\ra\tau\to\tau'}
\end{equation}

\begin{equation}	% parenthesised type
%\label{partype-rule}
\frac{\C\ts\ty\ra\tau}
     {\C\ts\partype\ra\tau}
\end{equation}
\comments
\begin{tabbing}
(\ref{constype-rule}) \= Recall that for $\tauk\theta$ to be defined, $\theta$
must have arity $k$.
\end{tabbing}

\rulesec{Type-expression Rows}{\C\ts\labtys\ra\varrho}
%\fbox{$\C\ts\labtys\ra\varrho$}
\begin{equation}	% record type components
%\label{longlabtys-rule}
\frac{\C\ts\ty\ra\tau\qquad\langle\C\ts\labtys\ra\varrho\rangle}
     {\C\ts\longlabtys\ra\{\lab\mapsto\tau\}\langle +\ \varrho\rangle}\index{32.15}
\end{equation}
\comment The syntactic constraints ensure $\lab\notin\Dom\varrho$.
%\caption{Rules for Types}
%\end{figure}

\subsection{Further Restrictions}
\label{further-restrictions-sec}
There\index{32.2} are a few restrictions on programs which should be enforced by a
compiler, but are better expressed apart from the preceding
Inference Rules.  They are:
\begin{enumerate}
%poly
%The following restriction has been removed from Version 1 because
%of polymorphic references and exceptions
%\item \label{monotypes-res}
%The reference value constructor ~{\tt ref}~ may occur in patterns
%with polymorphic type, but in an expression it must always elaborate to
%a monotype, i.e. a type containing no type variables.  
%Moreover, exception constructors can have monotypes only.
%These restrictions
%will be relaxed in future Versions, but some restrictions will always be
%necessary to ensure soundness of the type discipline.
\item For each occurrence of a record pattern containing a record wildcard,
i.e. of the form
%\begin{quote}
\verb+{+${\it lab}_1$\ml{=}$\pat_1$\ml{,}$\cdots$\ml{,}${\it lab}_m$\ml{=}$\pat_m$\ml{,}\verb+...}+
%\end{quote}
the program context must determine uniquely the domain
$\{{\it lab}_1,\cdots,{\it lab}_n\}$
of its record type, where $m\leq n$; thus, the context must
determine the labels $\{{\it lab}_{m+1},\cdots,{\it lab}_n\}$ of the fields
to be matched by the wildcard. For this purpose, an explicit type
constraint may be needed.  This restriction is necessary to ensure the
existence of principal type schemes.
\item In a match of the form ${\it pat}_1$ \ml{=>} $\exp_1$ \ml{|}$\;\cdots\;$
\ml{|} ${\tt pat}_n$ \ml{=>} $\exp_n$ 
the pattern sequence $\pat_1,\ldots,\pat_n$ should be {\sl irredundant};
that is, each $\pat_j$ must match some value
(of the right type) which is not matched by $\pat_i$ for any $i<j$.
In the context {\fnexp}, the $\match$ must also be {\sl exhaustive}; that is,
every value (of the right type) must be matched by some $\pat_i$.
The compiler must give warning on violation of these restrictions, 
but should still compile the match. 
The restrictions are inherited by derived forms; in particular,
this means that in the function binding\index{33.1}
 $\var\ \atpat_1\ \cdots\ \atpat_n\langle : \ty\rangle$\ \ml{=}\ $\exp$
(consisting of one clause only), each separate $\atpat_i$ should be
exhaustive by itself.
%must be {\sl irredundant} and {\sl exhaustive}.  That is, each ${\it pat}_j$
%must match {\sl some} value (of the right type) which is not matched by
%${\it pat}_i$ for any $i <j$, and {\sl every} value (of the right type) must be
%matched by some ${\it pat}_i$. The compiler must give a warning on violation
%of this restriction, but should still compile the match.
\end{enumerate}


\subsection{Principal Environments}
\label{principal-env-sec}
The\index{33.15} notion of {\sl enrichment}, $\E\succ\E'$, between environments
$\E=(\SE,\TE,\VE,\EE)$ and $\E'=(\SE',\TE',\VE',\EE')$ is defined
in Section~\ref{enrichment-sec}. For the present section,  $\E\succ\E'$
may be taken to mean $\SE=\SE'=\emptymap$, $\TE=\TE'$,
$\EE=\EE'$, $\Dom\VE=\Dom\VE'$ and, for each $\id\in\Dom\VE$,
$\VE(\id)\succ\VE'(\id)$.

Let\index{33.2} $\C$ be a context, and suppose that $\C\ts\dec\ra\E$
according to the preceding Inference Rules. Then $E$ is {\em principal}
(for $\dec$ in the context $\C$) if, for all $\E'$ for
which $\C\ts\dec\ra\E'$, we have $\E\succ\E'$. We claim that if
$\dec$ elaborates to any environment in $\C$ then it elaborates to
a principal environment in $\C$. Strictly, we must allow for the
possibility that type names and imperative type variables
which do not occur in $\C$ are chosen
differently for $\E$ and $\E'$. 
The stated claim is therefore made up to such variation.