Explain why we use a heap encoding.

1 files changed, 8 insertions, 4 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 6d339bd..29929d5 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -120,12 +120,16 @@ naturals. The idea is that the heap index describes the path taken through the
 term to reach a particular point, whilst the pointers describe the next step
 along the path.
 
+We choose to use a heap encoding over another encoding strategy for the
+following reasons. Firstly, inductive types in \lang{} can contain higher-order
+data, such as our tree of functions, which prevents us from using G\"odel
+encodings. Using a local translation makes writing the encoding easier, and as
+System~T does not have polymorphism, we cannot use Church encodings. We need to
+be able to write the fold operation, so we cannot use eliminator encodings. Thus
+the only suitable encoding strategy is a heap encoding.
+
 \TODO{
   \begin{itemize}
-    \item describe that storing higher-order data makes G\"odel encodings
-      impractical
-    \item describe that the need for local encodings rules out Church encodings
-    \item describe that the need for fold invalidates using codata encodings
     \item explain that using nat-list indices reflects the structure of terms
     \item give the encoding of roll
     \item give the encoding of fold