diff options
Diffstat (limited to 'sec/reducer.ltx')
-rw-r--r-- | sec/reducer.ltx | 12 |
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} |