summaryrefslogtreecommitdiff
path: root/sec/reducer.ltx
diff options
context:
space:
mode:
Diffstat (limited to 'sec/reducer.ltx')
-rw-r--r--sec/reducer.ltx12
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}