Describe why roll is hard to encode.

1 files changed, 10 insertions, 3 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 84ec4a5..0e7b244 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -50,11 +50,18 @@ let compose tree = foldmatch tree with
 \end{systemt}
 \end{listing}
 
+\subsection{Phase 1: Simplifying Roll}%
+\label{subsec:simplify-roll}
+
+Recall the typing judgement for \roll{} in \cref{fig:lang-ty}. The premise has
+type \(\sub{A}{X/\mu X. A}\). One consequence of the use of substitution is that
+inductive values can appear scattered throughout a term of this type. Take the
+inductive type \(\mu X. (1 + \nat \times X + \mu Y. 1 + X \times Y) \times (1 + X)\). A term of
+this type can have any number of inductive values, located in distant parts of
+the term.
+
 \TODO{
   \begin{itemize}
-    \item state that the initial type of roll makes it hard to encode
-    \item explain that there could be an arbitrary number of recursive arguments
-      scattered in a term
     \item describe that collecting them into one location makes future encoding
       steps easier
     \item justify why I add lists as a built-in type former