From af1438fade9bd56c5a1763165b3af71ce7fa6f32 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 7 May 2025 14:55:04 +0100 Subject: Describe union encodings. --- sec/encoding.ltx | 24 +++++++++++++++--------- 1 file 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} -- cgit v1.2.3