From af1438fade9bd56c5a1763165b3af71ce7fa6f32 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 7 May 2025 14:55:04 +0100
Subject: Describe union encodings.

---
 sec/encoding.ltx | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

(limited to 'sec/encoding.ltx')

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}
-- 
cgit v1.2.3

