diff options
| -rw-r--r-- | sec/encoding.ltx | 7 |
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 |