From 4677bd1af681e992b560b1061837c50f826c8bf7 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 30 Apr 2025 14:53:31 +0100
Subject: Justify the `index` operator.

---
 sec/encoding.ltx | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index d4fc90c..6e3f362 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -183,9 +183,19 @@ inductive type. Fortunately there exist encodings for lists such that
 not only does \(\mathsf{snoc}\) avoid recursion, but it is also as
 performant as cons.
 
+Adding the \(\mathsf{index}\) operator should also cause no
+issues. The biggest problem is deciding the result if the index is out
+of bounds. Two approaches taken from other programming languages
+include throwing an exception~\cites{exception} or returning an
+optional value~\cites{optional}. System~T does not have exceptions as
+a primitive, and returning an option doesn't help us consume the
+value. Instead we return an arbitrary inhabitant of the type, possible
+because all System~T types are inhabited. Regardless, one could prove
+that our encoding never calls \(\mathsf{index}\) with an out-of-bounds
+index.
+
 \TODO{
   \begin{itemize}
-    \item justify the index operator
     \item justify the head operator
   \end{itemize}
 }
-- 
cgit v1.2.3

