diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 482c7b0..5537a2e 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -245,6 +245,16 @@ following operators for lists: \(\mathsf{nil}\), \(\mathsf{cons}\), operators using only the \(\mathsf{length}\) and \(\mathsf{index}\) eliminators. +More formally, we encode the type \(\mathsf{List}~A\) by the type +\(\nat \times (\nat \to A)\), where the first component is the length of the +list and the second is the index function. We will justify using these +eliminators by giving an encoding for each operator. Starting with the +constructors, we can encode \(\mathsf{nil}\) by the pair \(\tuple{0, + \arb}\). The empty list has length zero, and as there are no valid +indices, we can give an arbitrary indexing function. Recall that all +System~T types are inhabited which allows us to construct this +arbitrary value. + \TODO{ \begin{itemize} \item explain why a list is a pair of length and index function |