diff options
| -rw-r--r-- | sec/systemt.ltx | 14 |
1 files 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 |