From bd68330d659f1d722f47a843571438389b3d02d5 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 24 Jun 2025 18:28:17 +0100 Subject: Fix 175--182. --- sec/systemt.ltx | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'sec/systemt.ltx') diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 1295654..041f89b 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -206,12 +206,13 @@ fold. \subsubsection*{Church Encodings} -Typically used in untyped settings, Church encodings represent data by their -fold operation. For example binary trees are Church encoded by the type \(\forall A. -(\nat \to A) \to (A \to A \to A) \to A\). The first argument describes how to deconstruct -leaves, and the second applies the inductive step on branches. This encoding -makes implementing fold trivial. Constructors for the inductive types are also -simple to encode, as demonstrated by the following example: +Typically used in untyped settings, Church encodings represent data by +their fold operation~\cite{church}. For example binary trees are +Church encoded by the type \(T = \forall A. (\nat \to A) \to (A \to A \to A) \to +A\). The first argument describes how to deconstruct leaves, and the +second applies the inductive step on branches. This encoding makes +implementing fold trivial. Constructors for the inductive types are +also simple to encode, as demonstrated by the following example: \begin{align*} \mathsf{leaf}(n) &\coloneq \lambda l, b.~l~n & -- cgit v1.2.3