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