Explain intrinsically well-scoped syntax.

1 files changed, 16 insertions, 1 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 0948073..9be1908 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -24,12 +24,27 @@ three main components:
     guarantee it will only ever have to process well-typed terms.
 \end{itemize}
 
+We present a simplified form of the Idris types used in the compiler.
+
 \subsection{Parser}
 \TODO{
   \begin{itemize}
     \item summarise \textcite{bidir}
     \item explain dependent state
-    \item explain what intentionally well-scoped syntax is
+  \end{itemize}
+}
+
+The parser returns an intrinsically well-scoped
+term~\cite{iwss}. Terms are a dependent data type with signature
+\verb|Context -> Type|. All variable names within a term are
+guaranteed to be bound within the context parameter or a term
+constructor such as \letkw{} or \foldkw{}. The term is
+\emph{intrinsically} well-scoped because the binding rules are
+enforced by the term constructors; an extrinsically well-scoped term
+would use a separate predicate to prove raw syntax is well-scoped.
+
+\TODO{
+  \begin{itemize}
     \item justify why I used intentionally well-scoped syntax
   \end{itemize}
 }