diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index fd71af8..becab5e 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -199,21 +199,16 @@ These operators satisfy the following equations: \end{align*} Computing the maximum value from a list is necessary to correctly -determine the recursive depth to use when folding over an inductive -value. It is also the primary reason why infinite inductive types are -forbidden. Take for example the inductive type \(\mu X. 1 + (\nat \to -X)\) of countable trees. To compute the recursive depth, we need to -compute the maximum of a countable sequence, which is impossible in -general. Thus we cannot encode such infinite types. - -We need the \(\mathsf{snoc}\) operation to find the indices of -inductive components within the encoding of \foldkw{}. This is true -even if we computed paths eagerly during \roll*{}; we need -\(\mathsf{snoc}\) to fixup paths there instead. - -The final operator we add at this phase is \(\mathsf{match}\) on -lists. We need this to determine whether a path is addressing the root -entry or one of its inductive components. +determine the recursive depth to use when folding over a value. It is +also the primary reason why infinite inductive types are +forbidden. Recall the inductive type \(\mu X. 1 + (\nat \to X)\) of +countable trees. To compute the recursive depth of such a tree, we +need to compute the maximum of an arbitrary countable sequence. Thus +we cannot encode such infinite types. + +We also add \(\mathsf{match}\) on lists. We need this to determine +whether a path is addressing the root entry or one of its inductive +components. We now return to our examples. After some beta reduction we recover the following value for \systemtinline{balanced}: |