From e9c892020fbc92584321503ed5202d16de0b5923 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 24 Jun 2025 18:36:15 +0100 Subject: Fix 230--234. --- sec/systemt.ltx | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/sec/systemt.ltx b/sec/systemt.ltx index cec4344..8b24706 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -288,10 +288,11 @@ constructors. For example, we can add the constructor \mathsf{double}(x) \coloneq \tuple{2 \cdot x.0, x.1} \] -Eliminator encodings inherit the weaknesses of Church encodings. Defining an -arbitrary fold requires polymorphism. Pattern matching is also impossible in the -general case. With our sum and depth example, we have no way of knowing whether -the value representing a tree came from a leaf or branch as we deliberately +Eliminator encodings inherit and extend the weaknesses of Church +encodings. Defining an arbitrary fold requires polymorphism in +general. Pattern matching is also impossible in the general case. With +our sum and depth example, we have no way of knowing whether the value +representing a tree came from a leaf or branch as we deliberately forget this information. \subsubsection*{Heap Encodings} -- cgit v1.2.3