diff options
Diffstat (limited to 'sec/systemt.ltx')
| -rw-r--r-- | sec/systemt.ltx | 13 |
1 files changed, 7 insertions, 6 deletions
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 & |