Initial introduction draft

1 files changed, 45 insertions, 17 deletions

diff --git a/sec/intro.ltx b/sec/intro.ltx
index f520bc4..d83b19f 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -4,23 +4,51 @@
 \section{Introduction}%
 \label{sec:intro}
 
-\TODO{
-\begin{itemize}
-  \item System~T is a STLC with natural numbers and primitive
-    recursors
-  \item Arguably simplest system for higher order computation
-  \item Explore expressive power by creating lang. encodes into Sys~T
-  \item \lang{} adds regular types to Sys~T
-  \item Example: compose binary tree of functions
-  \item Explain weird fold syntax
-  \item All \lang{} programs strongly normalise
-  \item Can do most programming
-  \item Write encoding alg. in \lang{}
-  \item Write fuelled Sys~T reducer
-  \item Developing non-trivial progs needs good tools
-  \item Have a certifying type checker and a compiler
-\end{itemize}
-}
+System~T is a simply-typed lambda calculus (STLC) with natural numbers
+and primitive recursors. It is arguably the simplest system for
+higher-order computation~\cite{stlc-simple}. In this paper we explore
+the expressive power of System~T by designing a new language that
+encodes into System~T.
+
+Our language, \lang{}, adds the regular types~\cite{regular} to
+System~T. These include sums, products and some inductive types. Below
+is a small pseudocode snippet of \lang{}. The function takes a binary
+tree with leaves labelled by unary functions on naturals and outputs
+their right-to-left composition.
+\begin{listing}[H]
+  \begin{systemt}
+let compose (tree : Tree) = foldmatch tree with
+  Leaf f         => f
+| Branch (f , g) => fun x => f (g x)
+  \end{systemt}
+  \vspace{-\baselineskip}
+\end{listing}
+This function has a major difference from the usual recursive
+definitions you would give in other functional languages. We never
+explicitly call \systemtinline{compose} in the inductive case. Instead
+the \systemtinline{fold} keyword eagerly applies the body to all
+inductive components in the argument. In this example, when we have a
+\systemtinline{Branch}, the left and right subtrees are eagerly passed
+to \systemtinline{compose}, so the body can only access the resulting
+functions \systemtinline{f} and \systemtinline{g}.
+
+\TODO{Why weird fold syntax}
+
+As we can encode all \lang{} programs into System~T, \lang{} inherit
+some of System~T's metatheory for free. In particular, as System~T is
+strongly normalising~\cite{syst-sn}, all \lang{} programs must
+terminate. Requiring programs terminate and are well-founded does not
+appear to greatly restrict what programs you can write in \lang{}. As
+evidence of this, we have written the encoding algorithm from \lang{}
+to System~T within \lang{}. We have also produced a fuelled System~T
+reducer; given enough fuel, it strongly normalises any well-typed
+System~T term.
+
+Developing these non-trivial recursive programs requires good tools
+for using \lang{}. To that end, we have implemented a certifying type
+checker and a compiler into Scheme. Our type checker not only checks
+whether a \lang{} program is well/ill-typed, but it also provides a
+proof for its decision.
 
 \subsubsection*{Contributions}%
 In this paper we: