Give bidirectional typing rules.

1 files changed, 78 insertions, 0 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index c7e161c..7b17ff7 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -93,6 +93,84 @@ creating the well-scoped AST, the raw AST cannot have been used in any
 prior computations, so we do not need to reference the raw AST.
 
 \subsection{Bidirectional Type Checker}
+
+\begin{figure}
+  \[
+  \begin{array}{cccc}
+    \begin{prooftree}
+      \hypo{x : A \in \Gamma}
+      \infer1{\judgement{\Gamma}{x}[\Rightarrow]{A}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma, x : A}{t}[\Leftarrow]{B}}
+      \infer1{\judgement{\Gamma}{\lambda x.t}[\Leftarrow]{A \to B}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{f}[\Rightarrow]{A \to B}}
+      \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A}}
+      \infer2{\judgement{\Gamma}{f~t}[\Rightarrow]{B}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{A}}
+      \hypo{\judgement{\Gamma, x : A}{u}[\Leftrightarrow]{B}}
+      \infer2{\judgement{\Gamma}{\lettm{t}{x}{u}}[\Leftrightarrow]{B}}
+    \end{prooftree}
+    \\\\
+    \begin{prooftree}
+      \hypo{\rangeover{\judgement{\Gamma}{t_i}[\Leftrightarrow]{A_i}}{i}}
+      \infer1{\judgement{\Gamma}{\tuple{\rangeover{t_i}{i}}}[\Leftrightarrow]{\prod_i A_i}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\prod_i A_i}}
+      \infer1{\judgement{\Gamma}{t.i}[\Rightarrow]{A_i}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A_i}}
+      \infer1{\judgement{\Gamma}{\tuple{i, t}}[\Leftarrow]{\sum_i A_i}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\sum_i A_i}}
+      \hypo{\rangeover{\judgement{\Gamma, x_i : A_i}{t_i}[\Leftarrow]{B}}{i}}
+      \infer2{\judgement{\Gamma}{\casetm{t}{\tuple{i,x_i}}{t_i}{i}}[\Leftarrow]{B}}
+    \end{prooftree}
+    \\\\
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{A}}
+      \hypo{A = B}
+      \infer2{\judgement{\Gamma}{t}[\Leftarrow]{B}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A}}
+      \infer1{\judgement{\Gamma}{t : A}[\Rightarrow]{A}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Leftarrow]{\sub{A}{X/\mu X. A}}}
+      \infer1{\judgement{\Gamma}{\roll~t}[\Leftarrow]{\mu X. A}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\mu X. A}}
+      \hypo{\judgement{\Gamma, x : \sub{A}{X/B}}{u}[\Leftarrow]{B}}
+      \infer2{\judgement{\Gamma}{\foldtm{t}{x}{u}}[\Leftarrow]{B}}
+    \end{prooftree}
+  \end{array}
+  \]
+  \caption{Bidirectional typing rules for
+    \lang{}.\@ We say \(t\) synthesises type \(A\) when
+    \(\judgement{\Gamma}{t}[\Rightarrow]{A}\) and \(t\) checks at type \(A\) when
+    \(\judgement{\Gamma}{t}[\Leftarrow]{A}\). We use \(\Leftrightarrow\) when a term can both
+    synthesise and check at a type. All arrows must resolve in the
+    same direction within the rule.}\label{fig:bidir}
+\end{figure}
+
 \TODO{
   \begin{itemize}
     \item describe how type checking produces a derivation