From 3277ef1d166cc02db4636228fc91598d7f112b20 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 24 Jun 2025 18:31:07 +0100 Subject: Fix 194--216. --- sec/systemt.ltx | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 2930abf..b848db6 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -258,12 +258,14 @@ polymorphism requires a global analysis, replacing the polymorphic bound with a \subsubsection*{Eliminator Encodings} -This encoding strategy generalises Church encodings. Rather than encoding -inductive types by their folds, eliminator encodings represent inductive types -as a product of all their (contravariant) consumers. For example, if we know the -only operations we will perform on a binary tree are finding the sum of all -leaves and the depth of the tree. We can encode the binary tree as a pair \(\nat -\times \nat\), where the first value is the sum and the second is the depth. +This encoding strategy generalises Church encodings. Rather than +encoding inductive types by their folds, eliminator encodings +represent inductive types as a product of some of their +(contravariant) consumers~\cite{eliminator-enc}. For example, if we +know the only operations we will perform on a binary tree are finding +the sum of all leaves and the depth of the tree. We can encode the +binary tree as a pair \(\nat \times \nat\), where the first value is the +sum and the second is the depth. In this encoding, the constructors eagerly compute the results of eliminators. With our sum and depth example, we encode the -- cgit v1.2.3