diff options
| -rw-r--r-- | sec/intro.ltx | 28 |
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 |