Give example for products and unions.

1 files changed, 26 insertions, 1 deletions

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}