From 0b2bc89f5a42128770b7f13e0e2661bebd35f529 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 2 May 2025 15:51:40 +0100 Subject: Give the encoding of nil. --- sec/encoding.ltx | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 -- cgit v1.2.3