Describe union encodings.

1 files changed, 15 insertions, 9 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 83130ea..58f0918 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -473,15 +473,21 @@ cluttered to be useful. \TODO{suggest an alternative}.
 \subsection{Phase 6: Encoding Unions}%
 \label{subsec:unions}
 
-\TODO{
-  \begin{itemize}
-    \item state that we encode unions as functions with possibly unused
-      arguments
-    \item define the union on types in argument form
-    \item define the put operator
-    \item define the get operator
-  \end{itemize}
-}
+At this point, the only type former not present in System~T is the
+union type.\@ \textcite{oleg} gives an inductive encoding for binary
+unions. We instead use an encoding for unions derived from the
+argument form of types. Given we have a family of types \(A_i\) in
+argument form, their union is the concatenation \(A_1 ++ A_2 ++ \cdots ++
+A_n\). To inject type \(A_k\) into the union, we ignore the function
+arguments for all the other type constructors. To project type \(A_k\)
+out of the union, we pass \(\mathsf{arb}\) to all the other arguments.
+
+Using this argument-form union, we remove the need to perform
+induction on types, and only have to iterate over the number of types
+in the union. This also simplifies the proof that our encoding of the
+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.
 
 \subsection{Phase 7: Desugaring}%
 \label{subsec:desugar}