Justify the use of non-destructive folds.

1 files changed, 7 insertions, 5 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 82706ed..b1c597a 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -175,11 +175,13 @@ type \verb|S| and returns a term distributing an accumulator for
 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 justify use of destructive folds
-  \end{itemize}
-}
+From a language design standpoint, we could have chosen that \foldkw{}
+is non-destructive. The inductive hypothesis would have the form
+\(\sub{A}{X/(\mu X. A) \times B}\) for shape \(A\) and motive \(B\). This is
+exactly as expressive as the chosen type, with inductive hypothesis
+\(\sub{A}{X/B}\). We chose to use the simpler motive inductive
+hypothesis for two reasons: it has a simpler categorical semantics;
+many folds do not need the non-destructive argument.
 
 \TODO{
   \begin{itemize}