1 files changed, 16 insertions, 7 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 95d9be3..ff4bc5c 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -449,13 +449,22 @@ let compose' (depth, heap) =
 \subsection{Phase 5: Encoding Products}%
 \label{subsec:products}
 
-\TODO{
-  \begin{itemize}
-    \item state that we encode products as functions from naturals to unions
-    \item explain that products are heterogenous vectors
-    \item justify implementing products as homogenous functional vectors
-  \end{itemize}
-}
+We will continue following the work of \textcite{oleg} to encode away
+products. A product \(\prod_i A_i\) is encoded as a function \(\nat \to
+\bigsqcup_i A_i\) from indices to values. This is similar to the
+encoding for lists, with only a couple of small variations. First, we
+statically know the length of a product, so we do not need to include
+it within its type. Secondly, a product can store values from
+different types whilst a list is homogenous, so we need to use the
+union to make it homogenous.
+
+We encode tupling \(\tuple{\rangeover{t_i}{i}}\) as the case split \(\lambda
+x. \casetm{x}{i}{\mathsf{inj}~i~t_i}{i}\). The projection \(t.i\) is
+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}.
 
 \subsection{Phase 6: Encoding Unions}%
 \label{subsec:unions}