From d11250e5e1c6c812811613ab046e5afcc42fb38b Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 7 May 2025 15:03:35 +0100
Subject: Give example for products and unions.

---
 sec/encoding.ltx | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 58f0918..b697150 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -468,7 +468,21 @@ encoded as the application \(\mathsf{prj}~(t~i)~i\).
 
 At this phase the encodings of our example functions,
 \systemtinline{balanced} and \systemtinline{compose'}, become too
-cluttered to be useful. \TODO{suggest an alternative}.
+cluttered to be useful. Instead we will consider the
+\systemtinline{dupfirst} function, of type \((\nat \to \nat) \times \nat \to
+(\nat \to \nat) \times (\nat \to \nat) \times \nat\), which takes a pair of a
+function and value, and duplicates the first component of the pair.
+Originally defined as \systemtinline{let dupfirst t = (t.0, t.0, t.1)},
+after encoding products the function becomes
+\begin{listing}[H]
+\begin{systemt}
+let dupfirst t = fun x => match x with
+  0 => inj 0 (prj (t 0) 0)
+| 1 => inj 1 (prj (t 0) 0)
+| 2 => inj 2 (prj (t 1) 1)
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
 
 \subsection{Phase 6: Encoding Unions}%
 \label{subsec:unions}
@@ -489,6 +503,17 @@ union satisfies the required beta reduction rule. In exchange, our
 union encoding is neither idempotent nor commutative, and generally
 results in larger types than \posscite{oleg} encoding.
 
+The \systemtinline{dupfirst} example reduces to the following:
+\begin{listing}[H]
+\begin{systemt}
+let dupfirst t = fun x => match x with
+  0 => fun x y => t 0 x
+| 1 => fun x y => t 0 y
+| 2 => fun x y => t 1 arb
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
+
 \subsection{Phase 7: Desugaring}%
 \label{subsec:desugar}
 
-- 
cgit v1.2.3

