From 0ccd53de6e7ed7cbc8df51e24d136ab1a445aa4e Mon Sep 17 00:00:00 2001 From: Chloe Brown 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') 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