diff options
| -rw-r--r-- | sec/encoding.ltx | 12 |
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} } |