From 94b225bb7a503b0f2e2cadcc5bd1c55953c6c152 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 22 May 2025 15:14:13 +0100
Subject: Give example of fold shenanigans

---
 sec/reducer.ltx | 39 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

(limited to 'sec/reducer.ltx')

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 1751b91..82706ed 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -137,9 +137,46 @@ unannotated System~T terms as in \cref{lst:term-ty}. Each phase is
 accompanied by its own inductive types representing types and
 type-annotated terms.
 
+Folds in \lang{} are destructive---the inductive components used to
+generate the induction hypothesis are unnamed. This has some
+interesting interactions with encoding the \(\mathsf{distrib}\) term
+in phase one, and implementing the \mapkw{} pseudo-operator in phase
+two. Both of these functions are defined by induction on types with
+motives that are functions returning terms. This means that the
+inductive hypothesis for each branch consists of a type constructor
+filled with some number functions. To construct a term, we need not
+only the subterms provided by the induction hypothesis, but we also
+need the types of those subterms. To preserve this typing information,
+both \(\mathsf{distrib}\) and \mapkw{} must return a pair of type and
+term.
+
+\begin{listing}
+  \begin{verbatim}
+; Arrow p =>
+  let myTy = ~(Arrow <Dom: p.Dom.Ty []; Cod: p.Cod.Ty []>) in
+  < Ty:   \env => myTy
+  ; Term: \env, k, s => ~(Abs ~(Abs ~(Tup
+    [ <Ty: s;    Term: ~(Var 0)>
+    ; <Ty: myTy; Term: ~(Var 1)>])))
+  >
+  \end{verbatim}
+  \caption{The branch of \(\mathsf{distrib}\) corresponding to
+    function types.}\label{lst:distrib-arrow}
+\end{listing}
+
+As a concrete example, consider the branch of \(\mathsf{distrib}\)
+over a function type, shown in \cref{lst:distrib-arrow}. The induction
+hypothesis is a pair of motives generated from the domain and
+codomain. The motive is a pair of functions. The \verb|Ty| component
+takes an environment and returns a compiled type. The \verb|Term|
+component takes an environment, a chosen type variable \verb|k| and a
+type \verb|S| and returns a term distributing an accumulator for
+\verb|S| at index \verb|k| outside of the type constructor. Ideally,
+we would only need the \verb|Term| component of the pair. However, the
+type annotations needed for the tuple force us to also compute the types.
+
 \TODO{
   \begin{itemize}
-    \item show a ``non-destructive'' fold
     \item justify use of destructive folds
   \end{itemize}
 }
-- 
cgit v1.2.3