summaryrefslogtreecommitdiff
path: root/sec
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-06-12 16:46:26 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-06-12 16:46:26 +0100
commitc91d233093b085ffef22905bf9599d519da8d084 (patch)
tree163b7be0114d3ea86e161304b6fc49e469763655 /sec
parent85905c93f74238b056f4b0ee0864782947ae02a6 (diff)
Give bidirectional typing rules.
Diffstat (limited to 'sec')
-rw-r--r--sec/compiler.ltx78
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