Fix 24--30.

1 files changed, 15 insertions, 13 deletions

diff --git a/sec/intro.ltx b/sec/intro.ltx
index d586e80..9baaf3f 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -13,10 +13,10 @@ encodes into System~T.
 Our language, \lang{}, adds the regular types~\cite{regular} to
 System~T. These include sums, products and some inductive
 types. Whilst there are well-known techniques to encode most of these
-types in System~T, \lang{} is the first known language to do so
-automatically. Below is a small pseudocode snippet of \lang{}. The
-function takes a binary tree of unary functions and outputs their
-right-to-left composition.
+types in System~T~\cites{oleg}{longley-normann}, \lang{} is the first
+known language to do so automatically. Below is a small pseudocode
+snippet of \lang{}. The function takes a binary tree of unary
+functions and outputs their right-to-left composition.
 \begin{listing}[H]
   \begin{systemt}
 let compose (tree : Tree) = foldmatch tree with
@@ -25,16 +25,18 @@ let compose (tree : Tree) = foldmatch tree with
   \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}
+Note that we never explicitly call \systemtinline{compose} with a
+subtree. Instead the \foldkw{} eagerly recurses on all subtrees
+automatically. In this example, when our tree is a
+\systemtinline{Branch}, the fold composes each subtree into functions
+\systemtinline{f} and \systemtinline{g} respectively.
+
+Our \foldkw{} syntax is more similar to eliminators~\cite{eliminators}
+than the explicit recursion in other functional languages. We use this
+eliminator style to ensure all recursion is structural. If we used
+explicit recursion, we would need complex checks for structural
+recursion, like in Agda~\cite{agda} and Idris~2~\cite{idris}.
 
 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