diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index cd749a9..b27f9d5 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -373,9 +373,16 @@ Unions have two operators: \(\mathsf{inj}~i~t\) and have the beta reduction rule \(\mathsf{prj}~(\mathsf{inj}~i~t)~i = t\). If the two type indices are different then projection is stuck. +We encode the injection into a sum \(\tuple{i, t}\) by the pair +\(\tuple{i, \mathsf{inj}~i~t}\). We encode pattern matching +\((\casetm{t}{\tuple{i,x_i}}{t_i}{i})\) by the term \( +(\casetm{t.0}{i}{\sub{t_i}{x_i/\mathsf{prj}~t.1~i}}{i}) +\) performing a pattern match over the tag to find the correct branch +to take. The pattern match on the right will be desugared into a +sequence of equality tests in phase seven. + \TODO{ \begin{itemize} - \item justify why sums are tagged unions \item justify adding union types \item justify the case operator on naturals \end{itemize} |