Describe encoding of inductive types.

1 files changed, 9 insertions, 1 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index ffc868b..a8d0269 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -101,9 +101,17 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X
 that calls each accumulator within \(A\) in sequence. The definition is by
 induction on the well-formedness derivation.
 
+\subsection{Phase 2: Encoding Inductive Types}%
+\label{subsec:inductive-types}
+
+We use a modified heap encoding to encode regular types. We use a
+\(\mathsf{List}~\nat\)-indexed heap, but keep the pointers within terms as
+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.
+
 \TODO{
   \begin{itemize}
-    \item state that we encode inductive types as nat-list-indexed heaps
     \item describe that storing higher-order data makes G\"odel encodings
       impractical
     \item describe that the need for local encodings rules out Church encodings