diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index deddd37..b7029f3 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -465,9 +465,12 @@ it within its type. Secondly, a product can store values from different types whilst a list is homogeneous, so we need to use the union to make it homogeneous. -We encode tupling \(\tuple{\rangeover{t_i}{i}}\) as the case split \(\lambda -x. \casetm{x}{i}{\mathsf{inj}~i~t_i}{i}\). The projection \(t.i\) is -encoded as the application \(\mathsf{prj}~(t~i)~i\). +To encode products, we must fix an injection \(I \hookrightarrow \mathbb{N}\) for each set of +labels \(I\). As \(I\) is finite, we can compare a given index against +the representation \(i_\ell\) of each label \(\ell\). Thus a tuple +\(\tuple{\rangeover{\ell : t_\ell}{\ell}}\) is encoded as the case split \((\lambda +x. \casetm{x}{i_\ell}{\mathsf{inj}~\ell~t_\ell}{\ell})\). The projection \(t.\ell\) +is encoded as the application \(\mathsf{prj}~(t~i_\ell)~\ell\). At this phase the encodings of our example functions, \systemtinline{balanced} and \systemtinline{compose'}, become too |