%%\documentclass[preprint,onecolumn,10pt]{sigplanconf}  % Horrible one-column style
%%\documentclass[preprint]{sigplanconf}               % Two-column style
\documentclass[draft]{article} 
\usepackage{fullpage} 

\usepackage{enumerate}
\usepackage{abbrev}
%% \usepackage{theorem}
\usepackage{xspace}
\usepackage{denot}
\usepackage{prooftree}
\usepackage{afterpage}
\usepackage{float}
\usepackage{pstricks}

\usepackage{latexsym} 

\usepackage{amsfonts} 
\usepackage{amssymb} 
\usepackage{amsthm} 

% Local packages
\usepackage{code}
\usepackage{mdwlist} 



\newcommand{\text}[1]{\mbox{#1}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}


\theoremstyle{definition} 
\newtheorem{definition}{Definition}[section]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Floats

\renewcommand{\textfraction}{0.1}
\renewcommand{\topfraction}{0.95}
\renewcommand{\dbltopfraction}{0.95}
\renewcommand{\floatpagefraction}{0.8}
\renewcommand{\dblfloatpagefraction}{0.8}
%\setlength{\floatsep}{16pt plus 4pt minus 4pt}
%\setlength{\textfloatsep}{16pt plus 4pt minus 4pt}

% Figures should be boxed
%    *** Uncomment the next two lines to box the floats *** 
\floatstyle{boxed}
\restylefloat{figure}

% Keep footnotes on one page
\interfootnotelinepenalty=10000 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Indentation
\setlength{\parskip}{0.5\baselineskip plus 0.2\baselineskip minus 0.1\baselineskip}
\setlength{\parsep}{\parskip}
% \setlength{\topsep}{0cm}
\setlength{\parindent}{0cm}

\newcommand{\reach}[2]{\widehat{#1}(#2)}
\newcommand{\ftv}[2]{ftv^{#1}(#2)}

\newcommand{\completed}{{\color{red}{\bf Complete.}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \input{defs}
\input{abbrevmap}
\def\rulename#1{\textsc{#1}}
\def\ruleform#1{\fbox{\Large $#1$}}
%% \def\ruleform#1{\fbox{$#1$}}
\def\ol#1{\overline{#1}}
\def\nb{\penalty10000 \ }
\def\fiddle#1{\hspace*{-0.5ex}\raisebox{0.4ex}{$\scriptstyle#1$}}

\def\wts{\vdash^{\fiddle{\mathrm{poly}}}}
\def\wtt{}  % Empty for now.  
\def\wtp{\fiddle{pat}}
\def\inst{\fiddle{\mathsf{inst}}}
\def\subs{\fiddle{sub\sigma}}
\def\subr{\fiddle{sub\rho}}

%% dimitris: unboxing relation
\def\unb{\fiddle{unb}} 
\def\sfr{\fiddle{sfr}}

%% dimitris: stuff used in the proofs.tex
\newcommand{\trans}[2]{[\![#1]\!]_{#2}} 
\newcommand{\revtrans}[1]{[\![#1]\!]^{-1}}

%% super-unification symbol, fills the whole
\newcommand{\fills}{\ensuremath{<-}}


% ``\returns{x}'' generate ``=> x;''
% It's used in an algorithmic judgement like
%    (S1,A1) |- t \returns{result} (S2,A2)
\newcommand{\returns}[1]{\Rightarrow #1 ;}

% Tuples via overlines
\newcommand{\tup}[1]{\overline{#1}}     % tuple
\newcommand{\tupn}[2]{\overline{#2}^{#1}}     

% Box around a type
\def\tbox#1{#1} %%% \psframebox[framesep=1pt,linewidth=0.5pt]{#1}}
%% Double box around a type
\def\dbox#1{\psframebox[framesep=0.5pt, linewidth=0.5pt]{\psframebox[framesep=1pt,linewidth=0.5pt]{#1}}}

\def\maybebox#1{\psframebox[framesep=1pt,linewidth=0.5pt,linestyle=dotted, dotsep=1pt]{#1}}

%%% different classes of meta-variables
\newcommand{\svar}{\xi}
\newcommand{\rvar}{\zeta}
\newcommand{\tvar}{\alpha}

\newcommand{\vbar}{\; | \;}

\def\Laufer{L{\"a}ufer}
\def\version#1{\rlap{\quad\textsc{(V#1)}}{}}

\newcommand{\simon}[1]{\emph{[SPJ: #1]}}
\newcommand{\dimitriv}[1]{\emph{[DV: #1]}}
\newcommand{\sweirich}[1]{\emph{[SW: #1]}}
\newcommand{\AS}{\mathcal{A}}
\newcommand{\XS}{\mathcal{X}}



\newcommand{\btr}{\triangleleft} 

\newcommand{\xs}{\ol{x}}
\newcommand{\as}{\ol{a}}
\newcommand{\bs}{\ol{b}}
\newcommand{\cs}{\ol{c}}
\newcommand{\ds}{\ol{d}}
\newcommand{\es}{\ol{e}}
\newcommand{\fs}{\ol{f}}
\newcommand{\gs}{\ol{g}}

\newcommand{\alphas}{\ol{\alpha}}
\newcommand{\betas}{\ol{\beta}}
\newcommand{\gammas}{\ol{\gamma}}
\newcommand{\deltas}{\ol{\delta}}
\newcommand{\epsilons}{\ol{\epsilon}}
\newcommand{\zetas}{\ol{\zeta}}
\newcommand{\etas}{\ol{\eta}}
\newcommand{\omegas}{\ol{\omega}}

\newcommand{\taus}{\ol{\tau}}
\newcommand{\sigmas}{\ol{\sigma}}
\newcommand{\rhos}{\ol{\rho}}

\newcommand{\mlf}{\ensuremath{\mathsf{ML}^{\mathsf{F}}}\xspace}
\newcommand{\hmf}{\ensuremath{\mathsf{HM}^{\mathsf{F}}}\xspace}


%% nasty interaction between denot.sty and abbrev.sty
\def\denot#1{[\![ #1 ]\!]}
\newcommand{\erase}[1]{{\cal E}\denot{#1}}
\newcommand{\typeof}[1]{{\cal T}\denot{#1}}
\newcommand{\shsubs}{|-^{\fiddle{\mathsf{DM}}}}               % Shallow subsumption 
\newcommand{\dmsubs}{|-^{\subs}}            % just for now ... 

\newcommand{\sdwf}{|-^{\fiddle{\mathsf{sd}}}}               % Shallow subsumption 


\newcommand{\sid}{\forall a. a \to a} 
\newcommand{\sall}{\forall a b. a \to b} 

\newcommand{\fsubs}{\vdash^{\fiddle{\mathsf{F}}}} 
\newcommand{\fwtt}{\fsubs} 


\newcommand{\unif}{\doteq} 

\newcommand{\typing}[4]{{{#1} \vdash {#2} : {#3} \rightsquigarrow {#4}}}
\newcommand{\coerce}[3]{{#1}\rhd {#2}\; _{\by}  \; {#3}}
\newcommand{\by}{{\text{\small{\tt by}}} }
\newcommand{\instantiate}[3]{\text{\small{\tt instan}}\; {#1} \rhd {#2} \; _{\by} \;  {#3}}
\newcommand{\generalize}[4]{\text{\small{\tt generalize}}\; {#1} \vdash {#2} \lhd {#3} \; _{\by} \;  {#4}}
\newcommand{\function}[4]{\text{\small{\tt fun}}\; {#1} \rhd {#2} \to {#3} \; _{\by} \;  {#4}}
\newcommand{\cast}[2]{\text{\bf Cast}\;{#2}\;{#1}}
\newcommand{\Cast}[2]{\text{\tt cast}\;{#2}\;{#1}}
\newcommand{\fomega}{F$^\omega$}
\newcommand{\recon}[7]{{{#1};{#2} \vdash {#3}[{#4}] : {#5} \rightsquigarrow {#6}; {#7}}}
%% \newcommand{\types}[6]{{#1}{#2} \vdash {#3} : {#4}  \rightsquigarrow {#5} ; {#6}}
\newcommand{\types}[5]{{#1} \vdash {#2} : {#3} ; {#5}}
\newcommand{\context}[4]{{{#1} \models {#2} : {#3} \to {#4}}}
\newcommand{\means}[3]{\{ {#1} \} = {#2} \mapsto {#3}}
\newcommand{\decl}[6]{{{#1} \vdash {#2} = {#3} : {#4} \rightsquigarrow {#5} = {#6}}}
\newcommand{\constrain}[2]{{#1} \supset \hspace*{-.13in} \ast  \;\, {#2}}
\newcommand{\allt}[2]{\forall {#1}.{#2}}
\newcommand{\Allt}[2]{\Lambda {#1}.{#2}}


\newcommand{\base}[4]{{#1} \vdash {#2} : {#3} \rightsquigarrow {#4}}
\newcommand{\declBase}[6]{{{#1} \vdash {#2} = {#3} \rightsquigarrow {#4} = {#5} : {#6} }}
\newcommand{\poly}[5]{{#1} \vdash {#2} : {#3} \rightsquigarrow {#4}; {#5}}
\newcommand{\Sc}{\textsc{S}}
\newcommand{\prop}[4]{{#1} \vdash {#2} : {#3} \rightsquigarrow {#4}}
\newcommand{\propD}[3]{{#1} \vdash {#2} \rightsquigarrow {#3}}
\newcommand{\propP}[4]{{#1} \vdash {#2} \rightsquigarrow {#3} \rhd {#4}}
 
\begin{document}

\title{ ``Not Unless I Told You So"\\
Evidence-based impredicative type reconstruction}
\author{Tim Sheard \and Dimitrios Vytiniotis \and Simon Peyton Jones} 
\date{\today} 


%% \authorinfo{}{}{}
%%\authorinfo{Tim Sheard}{Portland State University}{sheard@cs.pdx.edu}
%%\authorinfo{Dimitrios Vytiniotis \and Simon Peyton Jones}{Microsoft Research}{\{dimitris,simonpj\}@microsoft.com}
% \toappear{Submitted to the International Conference on Functional Programming 2005 (ICFP'05)}
\maketitle
\makeatactive

\section{Introduction}

Many sophisticated type systems make use of impredicative polymorphism to both state
and maintain properties about programs \cite{ }. The language \fomega~ is considered
the gold standard for writing programs with impredicative polymorphism. Unfortunately, the
over head of writing programs in \fomega can be quite high. This is due to the following
features of \fomega 
.
\begin{itemize}

\item Every binding occurrence of a variable is annotated with its exact (possibly polymorphic) type.

\item Every monomorphic use of a polymorphic variable must include type applications which indicate
which concrete type instance that polymorphic variable assumes at that location.

\item Every definition of a polymorphic variable must explicitly abstract over its
polymorphic type variables.

\item Type inference for \fomega~ is undecidable, so even a monomorphic program must be
fully annotated. There is no pay as you go solution.

\end{itemize}

This adds considerably to what must me written by the programmer. In contrast, systems
written in a language supporting Hindley-Milner type inference, need no type
annotations whatever. In the experience of the authors of this paper, most programs
written by humans, which use impredicative polymorphism, are {\it mostly Hindley-
Milner}. I.e. only small parts of these programs make use of impredicativity. So it is
a shame that in order to use impredicativity, one must resort to the extreme verbosity
of languages like \fomega. There have been many attempts to design languages which live
in between the two extremes of \fomega~ and Hindley-Milner, that require only light-
weight annotations\cite{}. In this paper we join this distinguished company, by
extending the techniques developed in QML with several new strategies:

\begin{itemize} 

\item We employ an extremely simple type propagation pass in which type information is
syntactically pushed down to the leaves of the syntax tree. This pass does not try to
be complete, exact, or clever, but it is sound. If a type is pushed down to a leaf,
then that leaf must have that type if the program is well typed.

\item We annotate bindings in the type environment, which normally contains information
only about the types of term variables, with a single bit of information that describes
if the type has free type variables.

\item We collect constraints about use sites of term-variables with non-closed types,
and solving these constraints in a second pass. 

\item We solve the generated constraints using a new algorithm. This algorithm is based
upon a logic-program description of the properties the solutions must have for the
program to be well typed.

\end{itemize}

All three of these strategies are somewhat orthogonal, and it is possible to combine
them in various ways. In fact we develop a series of type systems. The goal is that as
the systems grow in complexity, the number of annotations required by the programmer
decreases, and the number of programs accepted as well typed increases. How do we know
that a program is well typed? By translating the annotated term into a \fomega~ term.
We claim that every \fomega~ term is the translation of some annotated term, so
we {\em lose nothing} in terms of expressivity, but each system implements a
mostly Hindley-Milner strategy which minimizes annotations so we {\em gain something}
in terms of ease of use.

\paragraph{Evidence based typing.}
Inferring the type of a program in
\fomega~ is undecidable, in part, because some variables can be assigned an infinite number
of incomparable types. Which type should be chosen? In our strategy, the constraints
are evidence that a term variable is used in a context that demands a certain
type. We need only search for the most general type (amongst the finite evidence)
which satisfies every constraint. \fomega, and hence our system as well, does not have
most general types. But we do find the most general type amongst the evidence. If the
programmer knows of a more general type, he is free to annotate the program to support
his knowledge. If the programmer writes a program which provides no evidence that
a term has a non Hindley-Milner type, then a Hindley-Milner type will be assigned,
or the program will be rejected. Our systems behave exactly like Hindley-Milner
systems in the absence of user annotations.

Our type-reconstruction algorithm takes a program in a input language that supports
light-weight type annotations and reconstructs a program in \fomega~ where
all type information is made explicit. The algorithm is evidence based. That is, type
reconstruction proceeds as in Hindley-Milner, unless there is specific evidence, i.e.
light weight type annotations or contexts, that demand some more
sophisticated typing is possible (or necessary). A simple example might best illustrate
this point.

{\small %ex1.nax
\begin{verbatim}
id x = x
f1 (x:(forall a. a -> Int)) = x 6
f2 y = (f1 y, y True)
\end{verbatim}}

There are no type annotations (or evidence to the contrary) so \verb+id+
is assigned the Hindley-Milner type \verb+(forall a:* . a -> a)+.
The light-weight annotation on the argument \verb+x+ of the function \verb+f1+ 
provides evidence that \verb+f1+ should have type: \verb+(forall a:* . a -> Int) -> Int+. 
The application of \verb+f1+ to the argument \verb+y+ in the definition of \verb+f2+
provides evidence that \verb+y+ should have type \verb+(forall a. a -> Int)+,
and the application \verb+(y True)+ provides evidence that \verb+y+
should have type \verb+(Bool -> b)+ for some type \verb+b+. What type should we choose
for \verb+y+? Choose the most general type (amongst the evidence) that works
for all use sites of \verb+y+, which is  \verb+(forall a. a -> Int)+. 
The translations of these terms into \fomega~ reconstructs
all the type information missing in the original terms: 
Type abstractions denote polymorphic terms.
Type annotations appear on
$\lambda$-bound variables. And every polymorphic term
used in a monomorphic context is specialized by applying
it to the types at which it is used.

{\small 
\begin{verbatim}
id: (forall a:* . a -> a)
id = (/\ a:* . \ (x:a) -> x)

f1: (forall a:* . a -> Int) -> Int
f1 = \ (x:(forall a:* . a -> Int)) -> (x [Int]) 6

f2: (forall a:* . a -> Int) -> (Int,Int)
f2 = \ (y:(forall a:* . a -> Int)) -> (f1 y,(y [Bool]) True)
\end{verbatim}}

 

\section{A Series of Incresingly Expressive Type-Systems}

In this section we introduce a series of increasingly expressive type-systems.
The goal is for each system to either (1) accept more programs than the previous
one, or (2) accept the same programs but use fewer annotations. Our base system
is a modification of QML\cite{}.

\subsection{QML}

QML is an elegant and expressive system that combines Hindley-Milner type inference
and impredicative types. It has several features worth discussing.

\begin{itemize}
\item It contains both type-schemes ($\Pi \xs . t$) and impredicative ($\forall \xs . t$) types. 
While similar, these are separate, and are used in different ways.
The type environment binds term variables to type schemes. Much as in Hindley-Milner
\verb+let+ bound variables are given polymorphic type-schemes, and $\lambda$-bound
variables are given monomorphic type schemes (the $\xs$ are always the empty sequence for
a monomorphic type schemes). Let bound variables are automatically
generalized, and any variable with a polymorphic type scheme is automatically
specialized at every use site.
 
\item The introduction and elimiation of terms with impredicative types ($\forall \xs . t$)
is always associated with an explicit annotation. These annotations include
an impredicative type and a term. For impredicative introduction (generalization), the type appears
before the term. For example $(\forall a . a -> a) (\lambda x . x)$ generalizes
$(\lambda x . x)$ to have the impredicative type $(\forall a . a -> a)$.

For impredicative elimination (specialization) the type appears after the term.
For example in the application $(id (\forall a . a -> a)) 5$, the function $(id (\forall a . a -> a))$
is specialized to the type $Int -> Int$ so that it can be applied to $5$.

\item The system is expressive enough to encode every \fomega term. It mixes Hindley-Milner
type inference with impredicative types. But the annotation burden to the programmer
is still quite high.

\end{itemize}

Our systems are an attempt to improve upon the QML solution by removing the distinction
between type-schemes and impredicative types, and by lessening the burden of explicitly
annotating the introduction and elimination of every term with an impredicative type.
The first strategy we use is similar to QML's use of type-schemes in the typing
environment, but more flexible: annotate every binding in the type environment
binding term variables to types with a single bit of information ($\ast$) if it
is a closed type, and ($\bullet$) if the type could have free type variables.
In our first base system this distinction is syntactically apparent. Variables
are either introduced by top-level declarations ($\ast$), or they $\lambda$-bound.
If they are $\lambda$-bound and have an annotation they are annotated with $\ast$, if they do not
they are annotated with $\bullet$.
In later systems this distinction will not always be syntatctically apparent.





\begin{figure}[!htp]\small
\[\begin{array}{llrll}
    \text{Types}          & \sigma,\rho, \tau   & ::= &  | a | \sigma \to \sigma |  @T@\;\sigmas | \forall\as @.@ \sigma   \\ 
    \text{Binding Annotations}   & \delta   & ::= & \bullet | \ast   \\
    \text{Environments} & \Gamma & ::= &  \cdot  | \Gamma,(x{:}^{\bullet} \sigma ) | \Gamma,(x{:}^{\ast}\sigma) \\ 
    \text{Input Terms} & e,f & ::= &  x |  e\;f |  \lambda x @.@ e | \lambda (x{:}\sigma) @.@ e | @poly@\;  \as . (e: \rho)  | (@instan@\; e \; \sigma) \\ 
    \text{Output (\fomega)} & u,v & ::= &  x |  u\;v | \lambda (x{:}\sigma) @.@ u  | e [ \sigmas] | \Allt{\as}{u} \\ 
    \text{Declaration}      & d   & ::= & x : \sigma | x = e \\
   \text{Programs} & P & ::= &  d ; P | e \\                        
\end{array}\] 

\[\begin{array}{c}
 \ruleform{ \base{\Gamma}{e}{\sigma}{u} }  \\ \\ 
 \prooftree

 (x{:}^{\bullet} \sigma) \in \Gamma 
 --------------------------------------{var$\bullet$}
 \base{\Gamma}{x}{\sigma}{x}

 ~~~~

 (x{:}^{\ast}\allt{\as}{\tau}) \in \Gamma \quad
  --------------------------------------{var$\ast$}
 \base{ \Gamma}{x}{\tau[\sigmas / \as]}{x[\sigmas]}

  
  ~~~~~   
 
 \base{\Gamma}{e_1}{\sigma_2 \to \sigma_1}{u_2} \quad
  \base{\Gamma}{e_2}{\sigma_2}{u_1} 
  ---------------------------------------------------------------------------{app} 
  \base{\Gamma}{e_1\;e_2}{\sigma_1}{ u_1 \; u_2 }


~~~~~
  \base{\Gamma,(x{:}^{\bullet} \sigma_1)}{e}{\sigma_2}{u}
  ----------------------------------------------------------------------------------{abs$\bullet$}
  \base{\Gamma}{\lambda x @.@ e}{\sigma_1 \to \sigma_2}{\lambda (x{:}\sigma_1) @.@ u}
 
 ~~~~
 

    \base{\Gamma,(x{:}^{\ast}\sigma_1)}{e}{\sigma_2}{u}
   ---------------------------{abs$\ast$}
  \base{\Gamma}{\lambda  (x{:}\sigma_1) @.@ e}{\sigma_1 \to \sigma_2}{\lambda  (x{:}\sigma_1) @.@ u}
  

~~~~~

  \base{\Gamma}{e}{\tau}{u} \quad \as \notin FV(\Gamma)
 -----------------------------------------------------------------{gen}
 \base{\Gamma}{@poly@ \; \as . (e: \tau)}{\allt{\as}{\tau}}{\Allt{\as}{u}}
 
~~~~

 \base{\Gamma}{e}{\allt{\as}{\tau}}{u}
 ----------------------------------{instan}
 \base{\Gamma}{@instan@ \;  e \; (\allt{\as}{\tau})}{\tau[\sigmas / \as ]}{u[\sigmas]}

 
\endprooftree 
\end{array}\] 

\[\begin{array}{c}
 \ruleform{ \declBase{\Gamma}{f}{e}{f}{u}{\sigma} }  \\ \\ 
 \prooftree
 
 
\base{\Gamma}{e}{\tau}{u}  \quad \as = FV(\tau)
 ----------------------------------------------------------------{decl}
 \declBase{\Gamma}{(f}{e)}{(f}{\Allt{\as}{u})}{\allt{\as}{\tau}}
 
 ~~~~~
\endprooftree 
\end{array}\] 

\caption{Base Language}\label{base}
\end{figure} 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\subsection{The Base System}
The syntax of our system is described in Figure \ref{base}.
The system is comprised of three  {\em languages}. A language of types, 
an input language, an output
language (\fomega).

{\bf Types.} The language of types includes type variables, function types,
type constructors (like $Unit$, $List$, etc.) and impredicative types.


{\bf Input.} Input-terms contain three forms of type annotation. Optional typing of lambda
bound variables ($\lambda (x{:}\sigma) . e$) introduces functions that expect
polymorphic arguments. The $@poly@$ annotation 
 ($@poly@\;  \as . (e: \rho)$)
controls the introduction of terms with
polymorphic types. It has the same use as the prefix annotation with an impredicative
type to a term in QML  ($(\forall \as . \rho)\; e$) . The $@instan@$ annotation
$(@instan@\; e \; (\forall \as . \sigma))$
controls the elimination of terms
with polymorphic types. It has the same use as the postfix annotation with an
impredicative type to a term in QML $(e \; (\forall \as . \sigma))$.

{\bf Output.} Output-terms are \fomega~. They annotate every bound variable
($\lambda (x{:}\sigma) @.@ u $) with its exact type.
Type application ($ e [ \sigmas]$) specializes type of a term from a polytype to an instance
of that type,  and type abstraction ($\Allt{\as}{u}$) generalizes the type of a term from
a monotype to a polytype.  

{\bf Declarations.} A declaration is either: (1) A typing declaration ($ x : \sigma$),
which is taken as an annotation of the programmers intent that the variable $x$
should have type $\sigma$. Or (2) A value declaration
($x = e$), which defines the the variable. Names introduced in previous declarations
are in scope in later declarations. Some times in our examples we write a declaration like
($f\;x\; y\; z = e$) which is shorthand for ($f = \lambda x . \lambda y . \lambda z . e$).

{\bf Programs.} Programs are a sequence of declarations follwed by an input-term, which
computes the programs meaning. 

A program is typed by first applying the type propogation rules of Figure \ref{fig:prop},
which push type information stated by the programmer (from either typing declarations
or annotations on $\lambda$-bound variables) down the syntax tree. Then rule {\small DECL}
(from Figure \ref{base}) is applied to each value declaration. This rule generalizes the type of each top level
declaration, and this type is $\ast$ bound in subsequent declarations.


\paragraph{Typing terms in the base system.} The judgement ($\base{\Gamma}{e}{\sigma}{u}$)
states that under environment $\Gamma$ the input-term $e$ has type $\sigma$ and
translates to the \fomega~ term $u$. The most interesting rules are
the rules that introduce and eliminate variables. 

Variable elimination is handled in the {\small Var$\ast$} and the {\small Var$\bullet$}
rules. In accordance with the base system's roots as a QML derivative, $\ast$ bound variables
are generalized, and $\bullet$ bound variables are not.

Variable introduction is handled by the {\small ABS$\ast$} and the {\small ABS$\bullet$}
rules. $\lambda$-bound variables with user annotations are $\ast$ bound, and 
$\lambda$-bound variables without user annotations are $\bullet$ bound. A consequence
of this is that a variable without an annotation can only be used at a monomorphic type.

The {\small GEN} and {\small INSTAN} rules mark explicit introduction and elimination
of terms with impredicative types.  Summarizing, the base system works much like
QML. One small but important benefit is that the base system needs fewer explicit
annotations to introduce terms with impredicative types. This power is due to the
type propogation phase, and the type propagation phase is effective because of the
$\ast$ versus $\bullet$ distinction in the typing environment.

The strategy of Figure \ref{base} follows the the general strategy used by Hindley-Milner
type inference with reconstruction. We differ from this strategy only if the programmer
indicates otherwise by the use of explicit annotations. Without annotations
(explict types on lambda bound variables, or the use of {\tt poly} or {\tt instan}), the following hold.

\begin{itemize}

\item Every variable use that is known to represent
a polymorphic term (i.e. $\ast$-bound) is reconstructed to include instantiantiation at a (possibly
different) specific type.

\item Every (non-annotated) $\lambda$-abstracted variable is assigned a single type. In
Hindley-Milner this type is always a mono-type. Here it may be a polytype, but a polytype
is chosen only if evidence supports that choice.

\item Polymorphic variables are introduced by let-binding and annotation. In our language,
let-binding generaliztion occurs automatically only for top level functions. Polytypes are
introduced in other ways, but always by user annotation, never automatically.

\end{itemize}




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{figure}[!htp]\small

\[\begin{array}{c}
 \ruleform{ \propP{\Gamma}{P}{P}{\Gamma} }  \\ \\ 
 \prooftree


------------------------------------------{envMain}
\propP{\Gamma}{e}{e}{\Gamma}


~~~~

\propP{\Gamma_1,(x :^{\ast} \sigma)}{P_1}{P_2}{\Gamma_2}
------------------------------------------{envTypeDecl}
\propP{\Gamma_1}{x : \sigma;P_1}{P_2}{\Gamma_2}

~~~~~


\propP{\Gamma_1}{P_1}{P_2}{\Gamma_2} \quad
\propD{\Gamma_1}{x = e_1}{x = e_2}
----------------------------------------------------{envValueDecl}
\propP{\Gamma_1}{x =e_1 ;P_1}{x = e_2; P_2}{\Gamma_2}

\endprooftree 
\end{array}\] 

\[\begin{array}{c}
 \ruleform{ \propD{\Gamma}{d}{d} }  \\ \\ 
 \prooftree

\prop{\Gamma}{e_1}{\sigma}{e_2}
------------------------------------------{propValueDecl$\ast$}
\propD{\Gamma,(x :^{\ast} \sigma)}{x = e_1}{x = e_2}

~~~~
\prop{\Gamma}{e_1}{?}{e_2}
------------------------------------------{propValueDecl$\bullet$}
\propD{\Gamma}{x = e_1}{x = e_2}


\endprooftree 
\end{array}\] 


\[\begin{array}{c}
 \ruleform{ \prop{\Gamma}{e}{\sigma}{e} }  \\ \\ 
 \prooftree


\prop{\Gamma}{e_1}{\rho}{e_2} 
------------------------------------------{propAbs}
\prop{\Gamma}{\lambda x . e_1}{\sigma \to \rho}{\lambda (x: \sigma) . e_2}

~~~~

(x:^{\ast} \sigma) \in \Gamma
------------------------------------{polvVar}
\prop{\Gamma}{x}{\allt{\as}{\tau}}{@poly@\; \as\; (x:\tau)}

~~~~~ 

(x :^{\ast} \sigmas_{n} \to \rho) \in \Gamma \quad  \prop{\Gamma}{e_{i}}{\sigma_{i}}{f_{i}}
------------------------------------------------------------------------------{propApp$\ast$}
\prop{\Gamma}{x \; \es_{n}}{?}{x \; \fs_{n}}


~~~~

\prop{\Gamma}{e_1}{?}{f_1} \quad  \prop{\Gamma}{e_2}{?}{f_2}
-----------------------------------------------------{propApp$\ast$}
\prop{\Gamma}{e_1 \; e_2}{?}{f_1 \; f_2}

~~~~~

------------------------------------{polyAbs}
\prop{\Gamma}{\lambda x . e}{\allt{\as}{\tau}}{@poly@\; \as\; ((\lambda x . e):\tau)}


~~~~~

(x :^{*} \allt{\as}{\sigmas_{n} \to \sigma}) \in \Gamma \quad  \prop{\Gamma}{e_{i}}{\sigma_{i}}{f_{i}}
-----------------------------------------{appBinary}
\prop{\Gamma}{x \; \es_{n}}{?}{@instan@\; (@poly@\; \as . (x\; \fs_{n}):\sigma) (\allt{\as}{\sigma})}



\endprooftree 
\end{array}\] 

\caption{Type Propogation Rules}
\label{fig:prop}
\end{figure} 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{Type Propogation.} The type propogation phase makes implicit type information
explicit. Thus fewer user annotations need to be explicit because an inference
phase adds them implicitly. Type propagation succeeds because it is an invariant maintained
by the system that type annotations contain complete information, and thus
the types of variables with $\ast$ bound types are completely known. Thus
contexts involving $\ast$ bound variables can propogate this type information. For
example in the program

{\small % ex2.nax
\begin{verbatim}
f1 (x:(forall a. a -> Int)) = x 6

f2 y z = f1 y
\end{verbatim}}

Type propagation discovers that in the body of \verb+f2+ the variable
\verb+f1+ is $\ast$ bound, and hence this requires the argument \verb+y+
to \verb+f1+ to have an impredicative type. Thus we propagate this information
by returning the following program after the propagation pass.

{\small  
\begin{verbatim}
f1 = \ (x:(forall a . a -> Int)) -> x 6

f2 = \ y -> f1 ((poly a . y: a -> Int))
\end{verbatim}}

Knowing the complete type of some variables in the typing environment can be exploited in
other ways to allow even fewer explicit annotations, which is the purpose of the next system
we present.




\subsection{The $\bullet$-Monomorphic, $\Gamma^{\ast}$ extension of the base system.}

In Figure \ref{base+1} we extend the base system by adding additional rules that exploit
the distinction between $\ast$-bound and $\bullet$-bound term variables. If all the 
free variables of a term are $\ast$-bound, then the type of that term can be
determined exactly. Thus we can compute some typing annotations, rather than making
them explicit. This further reduces the amount of explicit annotation required
by the programmer.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{figure}[!htp]\small
\[\begin{array}{llrll}
    \text{Types}          & \sigma,\rho, \tau   & ::= &  | a | \sigma \to \sigma |  @T@\;\sigmas | \forall\as @.@ \sigma   \\ 
    \text{Binding Annotations}   & \delta   & ::= & \bullet | \ast   \\
    \text{Environments} & \Gamma & ::= &  \cdot  | \Gamma,(x{:}^{\bullet} \sigma ) | \Gamma,(x{:}^{\ast}\sigma) | \Gamma^{*} \\ 
    \text{Input Terms} & e,f & ::= &  x |  e\;f |  \lambda x @.@ e | \lambda (x{:}\sigma) @.@ e | @poly@ \; \as . (e: \rho)  | (@instan@\; e \; \sigma) \\ 
                       &     &     &  (@poly@\; e) |  (@instan@\; e) | @let@ \; x = e\; @in@\; f\\
    \text{Output (\fomega)} & u,v & ::= &  x |  u\;v | \lambda (x{:}\sigma) @.@ u  | e [ \sigmas] | \Allt{\as}{u} \\ 
    \text{Declaration}      & d   & ::= & x : \sigma | x = e \\
    \text{Programs} & P & ::= &  d ; P | e \\                                           
\end{array}\] 

\[\begin{array}{c}
 \ruleform{ \base{\Gamma}{e}{\sigma}{u} }  \\ \\ 
 \prooftree

 (x{:}^{\bullet} \sigma) \in \Gamma 
 --------------------------------------{var$\bullet$}
 \base{\Gamma}{x}{\sigma}{x}

 ~~~~

 (x{:}^{\ast}\allt{\as}{\tau}) \in \Gamma \quad
  --------------------------------------{var$\ast$}
 \base{ \Gamma}{x}{\tau[\sigmas / \as]}{x[\sigmas]}


  ~~~~  
 
 \base{\Gamma}{e_1}{\sigma_2 \to \sigma_1}{u_2} \quad
  \base{\Gamma}{e_2}{\sigma_2}{u_1} 
  ---------------------------------------------------------------------------{app} 
  \base{\Gamma}{e_1\;e_2}{\sigma_1}{ u_1 \; u_2 }


~~~~~
  \base{\Gamma,(x{:}^{\bullet} \sigma_1)}{e}{\sigma_2}{u}
  ----------------------------------------------------------------------------------{abs$\bullet$}
  \base{\Gamma}{\lambda x @.@ e}{\sigma_1 \to \sigma_2}{\lambda (x{:}\sigma_1) @.@ u}
 
 ~~~~
 

    \base{\Gamma,(x{:}^{\ast}\sigma_1)}{e}{\sigma_2}{u}
   ---------------------------{abs$\ast$}
  \base{\Gamma}{\lambda  (x{:}\sigma_1) @.@ e}{\sigma_1 \to \sigma_2}{\lambda  (x{:}\sigma_1) @.@ u}
  

~~~~~

  \base{\Gamma}{e}{\tau}{u} \quad \as \notin FV(\Gamma)
 -----------------------------------------------------------------{gen}
 \base{\Gamma}{ @poly@ \;  \as . (e: \tau)}{\allt{\as}{\tau}}{\Allt{\as}{u}}
 
~~~~

 \base{\Gamma}{e}{\allt{\as}{\tau}}{u}
 ----------------------------------{instan}
 \base{\Gamma}{@instan@ \;  e \; (\allt{\as}{\tau})}{\tau[\sigmas / \as ]}{u[\sigmas]}
 

~~~~~

  \base{\Gamma^{*}}{e}{\tau}{u} \quad \as = FV(\tau)
 -----------------------------------------------------------------{gen*}
 \base{\Gamma}{@poly*@ \;  e}{\allt{\as}{\tau}}{\Allt{\as}{u}}
 
~~~~

 \base{\Gamma^{*}}{e}{\allt{\as}{\tau}}{u}
 ----------------------------------{instan*}
 \base{\Gamma}{@instan*@ \; e}{\tau[\sigmas / \as ]}{u[\sigmas]}
 

\endprooftree 
\end{array}\] 


\[\begin{array}{c}
 \ruleform{ \declBase{\Gamma}{f}{e}{f}{u}{\sigma} }  \\ \\ 
 \prooftree
 
 
\base{\Gamma}{e}{\tau}{u}  \quad \as = FV(\tau)
 ----------------------------------------------------------------{decl}
 \declBase{\Gamma}{(f}{e)}{(f}{\Allt{\as}{u})}{\sigma}
\endprooftree 
\end{array}\] 

\[\begin{array}{c}
 \ruleform{ {\small derivable \; rules} }  \\ \\ 
 \prooftree
 
 
 
  \begin{array}{c}
  e = @poly@ \;  \as . (e_1: \tau) \\
  \base{\Gamma}{e_1}{\allt{\as}{\tau}}{u_1} \\
  \base{\Gamma,(x:^{\ast} \allt{\as}{\tau})}{f}{\sigma_2}{u_2} \\
  \end{array} 
 ----------------------------------------------------------------------------------{let1}
   \base{\Gamma}{@let@\; x = e \; @in@ \; f}{\sigma_2}{(\lambda (x:\allt{\as}{\tau}).u_2)\; u_1}
 

  ~~~~
  
  \begin{array}{c}
   \base{\Gamma}{e}{\sigma_1}{u_1} \\
   \base{\Gamma,(x:^{\bullet} \sigma_1)}{f}{\sigma_2}{u_2} \\
  \end{array} 
  -------------------------------------------------------------{let2}
  \base{\Gamma}{@let@\; x = e \; @in@ \; f}{\sigma_2}{(\lambda x . u_2)\; u_1}
  
~~~~~  
  
  \begin{array}{c}
    \base{\Gamma^{*}}{e}{\tau}{u_1} \\
    \base{\Gamma,(x:^{*}\allt{\as}{\tau})}{f}{\sigma}{u_2} \\
    \as \notin FV(\Gamma)
  \end{array}  
    -------------------------------------------------------------{let3}
    \base{\Gamma}{@let@\; x = e \; @in@ \; f}{\sigma}{(\lambda (x: \allt{\as}{\tau}) . u_2) u_1}

~~~~

\base{\Gamma}{e}{\tau}{u} \quad
 \as \notin FV(\Gamma)
--------------------------------------{haskell}
\base{\Gamma}{(e : \allt{\as}{\tau})}{\tau [ \sigmas / \as ]}{(\Allt{\as}{u}) [\sigmas]}

     
~~~~~
 
   \base{\Gamma^{*}}{e_1}{\allt{\as}{(\sigma \to \rho})}{u_1} \quad
   \base{\Gamma^{*}}{e_2}{\sigma[\sigmas / \as]}{u_2} \quad
  ---------------------------------------------------------------------------{autoApp} 
  \base{\Gamma}{e_1\;e_2}{\rho[\sigmas / \as]}{ u_1[\sigmas] \; u_2 }

~~~~
 
  (x{:}^{\ast}\sigma) \in \Gamma 
  --------------------------------------{varPoly}
  \base{\Gamma}{@poly@\; x}{\sigma}{x}


\endprooftree 
\end{array}\] 

\[\begin{array}{c}
 \ruleform{ \Gamma \to \Gamma }  \\ \\ 
 \prooftree
 
 
 -----------------------------{$\ast\cdot$}
   \cdot^{*} \to \cdot
   
~~~~

\Gamma^{*} \to \Gamma_2
------------------------------------------{$\ast\bullet$}
(\Gamma,(x{:}^{\bullet} \sigma))^{*}  \to \Gamma_2

~~~~

\Gamma^{*} \to \Gamma_2
------------------------------------------{$\ast\ast$}
(\Gamma,(x{:}^{\ast}\sigma))^{*}  \to \Gamma_2 ,(x{:}^{\ast}\sigma)
  
\endprooftree 
\end{array}\] 

\caption{ $\bullet$Monomorphic $\Gamma^{*}$ Extension}
\label{base+1}
\end{figure} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
This sytem includes two new rules, {\small Gen$\ast$} and {\small INSTAN$\ast$}, and
several derived rules. These rules depend upon typing a term in an environment where all
the $\bullet$-bound variables have been removed. See the ($\Gamma \to \Gamma$) judgment
in Figure \ref{base+1} for the rules to compute $\Gamma^{\ast}$. If a term can be 
typed as such, ($\base{\Gamma^{\ast}}{e}{\sigma}{u}$), then every free variable must be $\ast$-bound, and the type returned
$\sigma$ will be completely known.

The rule {\small GEN$\ast$} supports mostly-implicit impredicative type introduction. A
term can be annotated with nothing more than the keyword $@poly*@$ to indicate that it
should have an impredicative type. This type is computed the same way that a polymorphic type
is computed for a declaration at top-level. The same invariant holds, the environment
needed to type the term has only closed types inside, so all free variables in
$\tau$ can be generalized.

The rule {\small INSTAN$\ast$} works in a similar manner and 
supports mostly-implicit impredicative type elimination. A
term can be annotated with nothing more than the keyword $@instan*@$ to indicate that it
it is expected to be a closed term with an impredicative type, and that we want to
use the term at an arbitrary instance of its type. This is similar in scope and effect to the
rule variable rule for $\ast$-bound variables {\small VAR$\ast$}.

The derivable rules explain how a form of $@let@$ polymorphism can be introduced into the language
as syntatctic sugar.


 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{figure}[!htp]\small
\[\begin{array}{llrll}
    \text{Types}          & \sigma,\rho, \tau   & ::= &  | a | \sigma \to \sigma |  @T@\;\sigmas | \forall\as @.@ \sigma   \\ 
    \text{Binding Annotations}   & \delta   & ::= & \bullet | \ast   \\
    \text{Environments} & \Gamma & ::= &  \cdot  | \Gamma,(x{:}^{\bullet} \sigma ) | \Gamma,(x{:}^{\ast}\sigma) | \Gamma^{*} \\ 
    \text{Constraints}   & \Sc & ::= & \emptyset | \{(x,\sigma,\omegas)\} | \{( \cdot ,\sigma,\omegas)\} | \Sc  \cup \Sc | \Sc_{x} \\
    \text{Occurence}    & \omega      & ::= & (\sigma,\gamma) \\
    \text{Coercions}    & \gamma & ::= &  @gen@\; \as | @spec@\;\sigmas \\
    \text{Input Terms} & e,f & ::= &  x |  e\;f |  \lambda x @.@ e | \lambda (x{:}\sigma) @.@ e | (@poly@\; e \; \sigma)  | (@instan@\; e \; \sigma) \\ 
                       &     &     &  (@poly@\; e) |  (@instan@\; e) \\
    \text{Output (\fomega)} & u,v & ::= &  x |  u\;v | \lambda (x{:}\sigma) @.@ u  | e [ \sigmas] | \Allt{\as}{u} \\ 
                        % @let@\;(x{:}\sigma) =u\;@in@\;v &   
   \text{Declaration}      & d   & ::= & x : \sigma | x = e \\
   \text{Programs} & P & ::= &  d ; P | e \\                                                
\end{array}\] 

\[\begin{array}{c}
 \ruleform{ \base{\Gamma}{e}{\sigma}{u} }  \\ \\ 
 \prooftree

 (x{:}^{\bullet} \sigma) \in \Gamma 
 --------------------------------------{var$\bullet$}
 \poly{\Gamma}{x}{\sigma_{i}}{@cast@ \; \gamma_{i} \; x}{\{(x,\sigma,\{(\sigma_{i},\gamma_{i}) \})\}}

 ~~~~

 (x{:}^{\ast}\allt{\as}{\tau}) \in \Gamma \quad
  --------------------------------------{var$\ast$}
 \poly{ \Gamma}{x}{\tau[\sigmas / \as]}{x[\sigmas]}{\emptyset}


  ~~~~~   
 
 \poly{\Gamma}{e_1}{\sigma_2 \to \sigma_1}{u_2}{\Sc_1} \quad
 \poly{\Gamma}{e_2}{\sigma_2}{u_1}{\Sc_2}
 ---------------------------------------------------------------------------{app} 
 \poly{\Gamma}{e_1\;e_2}{\sigma_1}{ u_1 \; u_2 }{\Sc_1 \cup \Sc_2}


~~~~~
  \poly{\Gamma,(x{:}^{\bullet} \sigma_1)}{e}{\sigma_2}{u}{\Sc}
  ----------------------------------------------------------------------------------{abs$\bullet$}
  \poly{\Gamma}{\lambda x @.@ e}{\sigma_1 \to \sigma_2}{\lambda (x{:}\sigma_1) @.@ u}{\Sc_{x}}
 
 ~~~~
 

    \poly{\Gamma,(x{:}^{\ast}\sigma_1)}{e}{\sigma_2}{u}{\Sc}
   ---------------------------{abs$\ast$}
  \poly{\Gamma}{\lambda  (x{:}\sigma_1) @.@ e}{\sigma_1 \to \sigma_2}{\lambda  (x{:}\sigma_1) @.@ u}{\Sc}
  

~~~~~

  \poly{\Gamma}{e}{\tau}{u}{\Sc} \quad \as \notin FV(\Gamma) \quad \text{wff}\;\Sc
 ----------------------------------------------------------------------------------{gen}
 \poly{\Gamma}{@poly@ \;  e \; (\allt{\as}{\tau})}{\allt{\as}{\tau}}{\Allt{\as}{u}}{\emptyset}
 
~~~~

 \poly{\Gamma}{e}{\allt{\as}{\tau}}{u}{\Sc} \quad \text{wff}\;\Sc
 ----------------------------------{instan}
 \poly{\Gamma}{@instan@ \;  e \; (\allt{\as}{\tau})}{\tau[\sigmas / \as ]}{u[\sigmas]}{\emptyset}
 

~~~~~

 \poly{\Gamma^{*}}{e}{\tau}{u}{\Sc} \quad \as \notin FV(\Gamma) \quad \text{wff}\;\Sc
 -----------------------------------------------------------------{gen*}
 \poly{\Gamma}{@poly@ \;  e}{\allt{\as}{\tau}}{\Allt{\as}{u}}{\emptyset}
 
~~~~

 \poly{\Gamma^{*}}{e}{\allt{\as}{\tau}}{u}{\Sc} \quad \text{wff}\;\Sc
 ----------------------------------{instan*}
 \poly{\Gamma}{@instan@ \; e}{\tau[\sigmas / \as ]}{u[\sigmas]}{\emptyset}

 
\endprooftree 
\end{array}\] 


\[\begin{array}{c}
 \ruleform{ \declBase{\Gamma}{f}{e}{f}{u}{\sigma} }  \\ \\ 
 \prooftree
 
 
\poly{\Gamma}{e}{\tau}{u}{\Sc}  \quad \as \notin FV(\tau) \quad \text{wff}\;\Sc
 ----------------------------------------------------------------{decl}
 \declBase{\Gamma}{(f}{e)}{(f}{\Allt{\as}{u})}{\sigma}
\endprooftree 
\end{array}\] 


\[\begin{array}{c}
 \ruleform{ u \to u }  \\ \\ 
 \prooftree
 
 ----------------------------------------------------------------{castSpec}
 @cast@\; (@spec@ \; \sigmas) u \to u[\sigmas]
 
 ~~~~
 ----------------------------------------------------------------{castGen}
 @cast@\; (@gen@ \; \as) u \to \Allt{\as}{u}
 
\endprooftree 
\end{array}\] 

\[\begin{array}{c}
 \ruleform{ \text{wff}\;\Sc }  \\ \\ 
 \prooftree

 \forall (\cdot,\sigma,\omegas) \in \Sc . \; (\exists (\sigma_{i},\gamma_{i}) \in \omegas) \; . \; \sigma = \sigma_{i}) \wedge
                                         (\forall (\sigma_{j},\gamma_{j}) \in \omegas \; . \; 
                                         (\sigma = \allt{\as}{\tau}) \wedge (\sigma_i = \tau[\sigmas / \as]) \wedge (\gamma_1 = @spec@\; \sigmas))
-----------------------------------{wff}
\text{wff}\;\Sc

\endprooftree 
\end{array}\] 


\caption{ $\bullet$Polymorphic $\Gamma^{*}$ Extension}
\label{base+2}
\end{figure} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
\subsection{The $\bullet$-Polymorphic, $\Gamma^{\ast}$ extension of the base system.}

In Figure \ref{base+2} we extend the base system with a constraint collection system.
Constraints are used to collect additional evidence that cannot be made explicit
with the syntactic type propagation phase.
In Figure \ref{base+2} we specify how constraint based evidence is collected for each bound variable.
The judgment $\types{\textsc{S}_{1}}{\Gamma}{e}{\sigma}{u}{\textsc{S}_{2}}$ should be
interpreted as: given initial evidence $\textsc{S}_{1}$, under the environment $\Gamma$ the
term $e$ has type $\sigma$ and transforms the evidence state to $\textsc{S}_{2}$.





Notable differences from a traditional constraint collecting static semantics include the
two different rules for $\lambda$-abstraction. The rule {\scshape abs$\bullet$} applies
when the $\lambda$-bound variable has no annotation.  Here the next unique location
$n$ is consumed, and the variable is bound to this location in $\Gamma$ using the $\bullet$
binding annotation. At the same time a new triple (corresponding to this binding occurrence)
is added to the constraint state. This is specified in the {\scshape push} rule. The
rule {\scshape abs$\ast$} applies
when the $\lambda$-bound variable is annotated with a type. Here the type is bound in $\Gamma$
using the $\ast$ binding annotation. Note the difference between the two rules,
{\scshape abs$\bullet$} binds a location in $\Gamma$, whereas  {\scshape abs$\ast$} binds
a type. The type corresponding to the most general type of a $\bullet$-bound variable appears in
the constraint state, not the environment $\Gamma$.

The rules {\scshape var$\bullet$} and {\scshape var$\ast$} specify what happens at
variable use sites. The rule  {\scshape var$\bullet$} applies to uses of variables
which are bound without typing information. A, new, possibly different type, $\sigma_{i}$, is chosen for
each occurrence of a variable. These types are collected in the constraint state (rule {\scshape insert}).
The rule  {\scshape var$\bullet$} applies to variable occurrences of
variables bound in annotated $\lambda$-abstractions. The usual Hindley-Milner strategy applies.
Each occurrence gets typed using some instance of the (possibly) polymorphic type, $\sigma$, 
$\ast$-bound in $\Gamma$ of that variable. The rule {\scshape varPoly} allows an occurrence
of an $\ast$-bound  variable to retain its polytype. Again polytypes are introduced only in
the presence of evidence (here, the $@poly@$ annotation).
 


\section{Using the collected constraints}

A program is a sequence of declarations $f = e$ followed by a {\em main} body which is a term.
Constraints are collected separately for each declaration. Automatic generaliztion
of declarations is one way polytypes are introduced. In fact this is the only
way a polytype can be introduced without evidence. The rule for typing a declaraton is found 
in Figure \ref{fig:decl:typing}.
The right-hand-side of the declaration equation, $e$, is first subject to cnstraint collection,
producing a type, $\rho$, and a constraint set, $\Phi$. This set of constraints is
 a set of triples $(n,\sigma,\sigmas)$, corresponding to the
binding site, $n$, the most general type for that variable, $\sigma$,
and the types of all use sites, $\sigmas$, of every lambda bound variable.
$\Phi$ is well formed, only if for every triple, the most general type, $\sigma$
appears amongst the use sit types, $\sigmas$. This is this is the {\em evidence based}
part of the system. A type not amongst the use-site types cannot be assigned as the most
general type of the variable bound at location $n$. In addition, every other use-site
type must be an instance of the most general type.




\end{document}
