diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 10 |
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 |