


\section{Eager Typechecking}

There are two variations on eager typechecking. 
They both implement pure Canonical LF, in the sense that
terms remain canonical throughout the typechecking process.
(We will admit non-canonical terms during lazy typechecking.)

The difference between the variations lies in the treatment
of substitutions. The first variation
considers substitutions as either a $\Shift^n$ or a $M\cdot\sigma$.
The second adds a ``lazy'' composition $\sigma_1\Comp\sigma_2$.
We write the rules for both versions together, as the majority
are identical.  Where there are extra rules needed for the
extra case of a substitution, they will be labelled as such.

%-------------------------------------------------------------------------------
% Terms                                                                         
%-------------------------------------------------------------------------------

\subsection{Terms}

$$
\begin{array}{llll}
\mathbf{Levels} & L & ::= & \Type \Spb \Kind \\
\mathbf{Expressions} & U,V & ::= & L \Spb \PiTyp{U_1}{U_2} \Spb \lambda U \Spb H\cdot S \\
\mathbf{Heads} & H & ::= & c \Spb i\\
\mathbf{Spines} & S & ::= & \Nil \Spb U;S\\
\mathbf{Eager\ Substitutions} & \sigma & ::= & M\cdot\sigma \Spb \Shift^n \\
\mathbf{Lazy\ Substitutions} & \sigma & ::= & M\cdot\sigma \Spb \Shift^n \Spb \sigma_1 \Comp \sigma_2\\
\end{array} 
$$


%-------------------------------------------------------------------------------
% Typecheck                                                                     
%-------------------------------------------------------------------------------

\subsection{Typechecking}

\bigskip 
\framebox{$\CheckTy{U}{V}$}
\bigskip 

$$
\begin{array}{cc}
\infer{\CheckTy{\Type}{\Kind}}{} &
\infer{\CheckTy{\PiTyp{A}{U}}{V}}{\CheckTy{A}{\Type} & \CheckTy[\Gamma,A]{U}{V}}\\\\
\infer{\CheckTy{c\cdot S}{V}}{\Sigma(c) = U & \Focus{S}{U}{V'} & \Equiv{V'}{V}} &
\infer{\CheckTy{\Lam{M}}{\PiTyp{A_1}{A_2}}}{\CheckTy[\Gamma,A_1]{M}{A_2}} \\\\
\infer{\CheckTy{i\cdot S}{A_2}}{\Gamma(i)=A_1 & \Focus{S}{A_1}{A_2'} & \Equiv{A_2'}{A_2}}
\end{array} 
$$

\bigskip 

\begin{Note}\label{context:shift} 
Note that you must shift the type you extract from $\Gamma$, as the
free variables (indices) should point to the slots before $i$.  Moving
the type $A$ from the context to the consequent must adjust the pointers.
We thus define $\Gamma(i) = A$ as the $i$th element of $\Gamma$
under $\Shift^i$.
\end{Note} 

\bigskip 
\framebox{$\Focus{S}{U}{V}$}
\bigskip 

$$
\begin{array}{lr}
\infer{\Focus{\Nil}{\Type}{\Type}}{} & 
\infer{\Focus{\Nil}{P}{P}}{} \\\\
\infer{\Focus{(M;S)}{\PiTyp{A}{U}}{V}}{\CheckTy{M}{A} & \Focus{S}{U[M\cdot\IdSub]}{V}}
\end{array} 
$$

%-------------------------------------------------------------------------------
% Substitutions                                                                 
%-------------------------------------------------------------------------------

\subsection{Substitutions}

(The notation $\Shift$ means $\Shift^1$, and $\IdSub$ means $\Shift^0$.)  

We \emph{apply} subsitutions to terms.

\bigskip
\framebox{$U\Msub = U'$}

\begin{align*} 
\Type\Msub &= \Type \\
(\PiTyp{A}{U})\Msub &= \PiTyp{(A\Msub)}{(U\Ssub)}\\
(c\cdot S)\Msub &= c\cdot (S\Msub) \\
(\Lam{M})\Msub &= \Lam{(M\Ssub)}\\
(i\cdot S)\Msub &= \begin{cases}
                     j\cdot S\Msub \mbox{\ if $i\Msub = j$} \\
                     M \App S\Msub\mbox{\ if $i\Msub = M$}
                   \end{cases} 
\end{align*} 



\framebox{$S\Msub = S'$}

\begin{align*} 
\Nil\Msub &= \Nil\\
(M;S)\Msub &= M\Msub;S\Msub
\end{align*} 

\framebox{$i\Msub = M$}
\bigskip 

This judgment is the first place we distinguish between 
the different notions of substitution.  The rule (*)
holds only for the second variant.

\begin{align*} 
1[M\cdot\sigma] &= M\\
n+1[M\cdot\sigma] &= n[\sigma]\\
i[\Shift^n] &= i+n\\
i[\sigma_1\Comp\sigma_2] &= (i[\sigma_1])[\sigma_2]\tag{*}
\end{align*} 

We still need the notion of beta reduction when a 
head gets instantiated with a lambda.  We show
only the possible cases.

\bigskip 
\framebox{$M \App S = M'$}

\begin{align*} 
(H\cdot S)\App\Nil &= H\cdot S\\
\Lam{M}\App(M';S) &= M[M'\cdot\IdSub]\App S
\end{align*} 

In the first case of eager typechecking, composition doesn't
have a syntactic existence.  Thus we need to carry out all 
compositions eagerly.  The rules for composing substitutions are:

\bigskip 
\framebox{$\sigma\Comp\sigma' = \sigma''$}

$$
\begin{array}{llll}
(M\cdot \sigma) & \Comp \sigma' &= &M[\sigma']\cdot (\sigma\Comp\sigma') \\
\Shift^n & \Comp \Shift^m &= &\Shift^{n+m}\\
\Shift^0 & \Comp \sigma &= &\sigma\\
\Shift^{n+1}&\Comp (M\cdot\sigma) &= &\Shift^n\Comp\sigma
\end{array} 
$$

%-------------------------------------------------------------------------------
% Equivalence                                                                   
%-------------------------------------------------------------------------------

\subsection{Equivalence} 

If we only allowed constant declarations in a signature then checking equivalence
of terms would be a simple matter of checking syntactic equality.  
With definitions of the form $c : A = M$, we must account
for the fact that a focusing phase might return a type $A$ to 
check against a type $A'$ that are not syntactically equal, but
if one expanded all the definitions and normalized the resulting
terms than they would be identical.  We thus need a judgment for the
equivalence of types $A$ and terms $M$.  (Since we are not allowing
type level definitions, we do not need to check for equivalent kinds.)

We use the judgment $c\StepsTo M$  to mean
that the constant $c$ has definition $M$. 

\bigskip 
\framebox{$\Equiv{U}{U'}$}
\bigskip 

$$
\begin{array}{lcr}\
\infer{\Equiv{U}{U'}}{\Equiv{U'}{U}} &  
\infer{\Equiv{\PiTyp{U_1}{U_2}}{\PiTyp{U_1'}{U_2'}}}{\Equiv{U_1}{U_1'} & \Equiv{U_2}{U_2'}} & 
\infer{\Equiv{c\cdot S}{c\cdot S'}}{\Equiv{S}{S'}} \\\\
\infer{\Equiv{\Lam{M}}{\Lam{M'}}}{\Equiv{M}{M'}} &
\infer{\Equiv{i\cdot S}{i\cdot S'}}{\Equiv{S}{S'}} &
\infer{\Equiv{c\cdot S}{M}}{c\StepsTo M' & \Equiv{M'@S}{M}} 
\end{array} 
$$

\bigskip 
\framebox{$\Equiv{S}{S'}$}
\bigskip 

$$
\begin{array}{lcr}
\infer{\Equiv{\Nil}{\Nil}}{} &
\infer{\Equiv{M;S}{M';S'}}{\Equiv{M}{M'} & \Equiv{S}{S'}}
\end{array} 
$$

\subsection{A Note on Implementing Equivalence Checking}

  For various reasons, we need equivalence checking to
be as fast as possible.  Equivalence checking is complicated
by notational definitions.  If checking $A=B$ fails, we might need
to expand definitions in one or both terms.  One could simply
expand all definitions to yield a sound algorithm, but this would
be horribly slow.  

  The solution given by Twelf, suggested by 
Pfenning and Reed, is to store two extra bits of information 
with each constant.  The first is the \emph{height} of a constant.
This merely records the definition depth of a constant.  Constants that
do not refer to other constants have height 0.  A constant $c$ that refers
to others has height $1 + \max\Set{\mbox{height of constants occuring in } c}$.
Note that only constants with the same height can be equal.  
The second bit of data is the \emph{root}, it{i.e.} the head of the term that would be obtained by 
expanding all definitions.  Note that any two equal terms must have the
same root after full expansion. 

These two bits of data yield a natural algorithm for determining 
equivalence of terms.  If, when checking equality of $A=B$,
we find that two constants must be equal for $A,B$ to
be equivalent, but are not syntactically equal, 
we check to see if the roots are the same.
If not, we fail.  Otherwise, we check the heights.  If the heights
differ, we expand the constant with the greater height until 
they are equal, and check again.  Once the levels
are equal, while the constants are still distinct, we 
expand both definitions, level by level, until all constants
are expanded.  In the worst case, this will take as much time
as expanding all the definitions.  In the usual case, however,
where the constants differ\footnote{indeed, unification fails
around \%80 of the time}, the clash will be found long before
the terms are fully expanded.  

This leads to an additional rule 

$$
\begin{array}{cccc}
\infer{\Equiv{c\cdot S}{c'\cdot S'}}{\Root(c)=\Root(c') & \Card{c} \geq \Card{c'} & c\StepsTo M' & \Equiv{M'@S}{c'\cdot S'}} 
\end{array} 
$$

where $\Card{c}$ is the height of $c$, and $\Root(c)$ is the root.
This holds in both the eager and lazy cases.
