From 4677bd1af681e992b560b1061837c50f826c8bf7 Mon Sep 17 00:00:00 2001 From: Chloe Brown 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