Explain how to fold.

1 files changed, 33 insertions, 1 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index e66f499..8fcedd1 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -285,7 +285,39 @@ sums in order to store the data for different constructors within a single type.
 \TODO{
   \begin{itemize}
     \item create box-and-pointer diagram
-    \item explain how to fold
+  \end{itemize}
+}
+
+The recursive depth is essential for the fold operation. We iteratively
+construct a heap of values; the recursive depth is an upper bound on the number
+of steps it takes to converge on the ``true'' result of the fold. For recursive
+depth zero, we return an arbitrary value at each index, and as no inductive
+value is made from applying zero constructors, we have no soundness obligations.
+It is possible to return an arbitrary value as all System~T types are inhabited.
+For the successor case, at any given index we look up the constructor and
+associated data in the heap. We use the recursively-constructed return heap to
+replace inductive arguments with suitable values, and then apply the appropriate
+fold operation.
+
+\[
+\dofoldmatch*{t}{
+  \mathsf{leaf}(n).      f(n);
+  \mathsf{branch}(x, y). g(x, y)
+} \coloneq
+\dolet
+  {\tuple{depth, root, heap}}{t}
+  {go}*{
+    \doprimrec*{depth}
+      {\arb{}}
+      {h}{\lambda i.
+        \domatch*{heap~i}{
+          \mathsf{Left}(n).     f(n);
+          \mathsf{Right}(j, k). g(h~i, h~j)}}}
+  *{go~root}
+\]
+
+\TODO{
+  \begin{itemize}
     \item explain how to roll
   \end{itemize}
 }