State we encode sums as tagged unions.

1 files changed, 6 insertions, 1 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 5dbe00f..c7506db 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -361,9 +361,14 @@ let compose (depth, heap) =
 \subsection{Phase 4: Encoding Sums}%
 \label{subsec:sums}
 
+In this phase we remove sums from the language by encoding them as
+tagged C-style unions, following the work of \textcite{oleg}. We
+encode the type \(\sum_i A_i\) by the pair \(\nat \times \bigsqcup_i A_i\), of
+a tag indicating which case we are in, and a union which can contain
+a value from any case.
+
 \TODO{
   \begin{itemize}
-    \item state that we encode sums as tagged C-style unions
     \item explain the operations and equations of unions
     \item justify why sums are tagged unions
     \item justify adding union types