From 0ccd53de6e7ed7cbc8df51e24d136ab1a445aa4e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 24 Apr 2025 13:02:31 +0100
Subject: Describe why roll is hard to encode.

---
 sec/encoding.ltx | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'sec/encoding.ltx')

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
-- 
cgit v1.2.3

