Outline bidirectional algorithm.

1 files changed, 48 insertions, 1 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 7b17ff7..decb2af 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -171,9 +171,56 @@ prior computations, so we do not need to reference the raw AST.
     same direction within the rule.}\label{fig:bidir}
 \end{figure}
 
+\Cref{fig:bidir} shows how we have modified the \lang{} typing rules
+for bidirectional type checking. The changes are
+standard~\cref{bidir}. Products can both check and synthesise types.
+The \rollkw{} operator can only be checked as there is no unique
+correct guess for the shape type. The body of a \foldkw{} must be
+checked. The induction hypothesis is added to the context, so its type
+must be known before processing the body. As the induction hypothesis
+is filled by the motive, the only mode-correct way to obtain the
+motive type is for \foldkw{} to be checked.
+
+The Idris~2 type for certifying the bidirectional judgement is almost
+a direct translation of the judgement in \cref{fig:bidir}. The
+differences are down to products and sums allowing permutations of
+their labels. Whilst on paper we can represent these \(n\)-ary types
+as sets, in Idris they are realised by lists. This discrepancy
+manifests in \lang{}'s type checker in three ways:
+\begin{itemize}
+  \item when switching from synthesis to checking, the synthesised and
+    expected types are compared up to reordering, instead of equality;
+  \item for case splits, we check there is a permutation between
+    variants and branches; and
+  \item for checking tuples, we check every label in the type has a
+    unique component in the tuple.
+\end{itemize}
+
+\TODO{describe how type checking produces a derivation}
+
+For error reporting we introduced Idris types for negative
+certifications. Values of these types indicate how the bidirectional
+algorithm failed. Consider synthesising the type of an
+application. A negative certificate has three possibilities:
+\begin{itemize}
+  \item the function does not synthesise a type;
+  \item the function's type is not a function type;
+  \item the argument does not check at domain type.
+\end{itemize}
+Negative certificates give a precise reason why the algorithm failed.
+
+We also designed negative certificates to report as many errors as
+possible. For example, when a tuple fails to check at a type, we can
+record all of the fields that fail to check, not only the first. We
+could enforce that negative certificates record all the errors by
+requiring a certificate (positive or negative) for every field.
+Because this guarantee is unnecessary for the rest of the compiler we
+have not done this. Our more lax certificates are still sufficiently
+expressive to prove a term cannot have both a positive and negative
+certificate.
+
 \TODO{
   \begin{itemize}
-    \item describe how type checking produces a derivation
     \item explain the derivation is runtime erased
     \item justify extrinsic derivation
     \item justify the derivation having no runtime cost