From d5409dd63799c494539497444313b1a7c08b8c8a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 27 May 2025 15:58:12 +0100
Subject: Justify the use of non-destructive folds.

---
 sec/reducer.ltx | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'sec')

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}
-- 
cgit v1.2.3