diff options
| -rw-r--r-- | sec/intro.ltx | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/sec/intro.ltx b/sec/intro.ltx index d83b19f..d586e80 100644 --- a/sec/intro.ltx +++ b/sec/intro.ltx @@ -11,10 +11,12 @@ 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. +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. \begin{listing}[H] \begin{systemt} let compose (tree : Tree) = foldmatch tree with |