Justify the `index` operator.

1 files changed, 11 insertions, 1 deletions

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}
 }