Describe distrib.

1 files changed, 27 insertions, 8 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 8087e20..ffc868b 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -72,15 +72,34 @@ the \roll*{} operator, which has the following type derivation:
 \]
 Rather than include the inductive values within the term to roll, they are
 instead gathered into an external list. The places that contained inductive
-values in the rolled term now contain indices into the list.
+values in the rolled term now contain indices into the list. The new operator
+satisfies the following equation:
+\[
+\dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u}
+\]
 
-\TODO{
-  \begin{itemize}
-    \item justify why I add lists as a built-in type former
-    \item describe the strength function, the key step in this phase
-    \item state it is defined by induction on the outer functor
-  \end{itemize}
-}
+\TODO{justify why I add lists as a built-in type former}
+
+To encode \roll{} into \roll*{} we require a function that traverses a term of
+type \(\sub{A}{X/\mu X. A}\) and collects all inductive values into a single list.
+We can extend a list with a single value and return the index of that value with
+the writer monad~\cite{writer}: \(\mathsf{extend} : A \to \mathsf{List}~A \to
+\mathsf{List}~A \times \nat\). By using the \mapkw{} operator we can replace all
+inductive values in a term \(\sub{A}{X/\mu X. A}\) with accumulator functions
+\(\sub{A}{X/\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times \nat}\). The
+non-trivial step is ``distributing'' the writer monad with the substitution to
+obtain a value of type \(\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times
+\sub{A}{X/\nat}\). We can apply this function to the empty list to obtain the
+arguments for \roll*{}.
+
+Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X \in
+\Psi\), a type environment \(\alpha\) and a type \(S\), we have a term
+\(\mathsf{distrib}\) defined in phase-one \lang{} of type
+\[
+\submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha}
+\]
+that calls each accumulator within \(A\) in sequence. The definition is by
+induction on the well-formedness derivation.
 
 \TODO{
   \begin{itemize}