1 files changed, 132 insertions, 0 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
new file mode 100644
index 0000000..84ec4a5
--- /dev/null
+++ b/sec/encoding.ltx
@@ -0,0 +1,132 @@
+\documentclass[../main.tex]{subfiles}
+
+\begin{document}
+\section{Encoding Artist}%
+\label{sec:embedding}
+
+\TODO{
+  \begin{itemize}
+    \item remind the reader why encoding into System~T is useful
+  \end{itemize}
+}
+
+There are seven phases in the encoding process. In general, each phase removes a
+specific type constructor until only naturals and function types remain.
+Sometimes removing types requires introducing others; we will introduce lists of
+naturals and C-style unions, which we will later need to remove. The full list
+of seven phases are:
+\begin{enumerate}
+\item changing the type of the \roll{} operator so that all recursive arguments
+  are collected together in a list.
+\item using a list-indexed heap encoding to represent inductive types.
+\item using an eliminator encoding to represent lists.
+\item introducing unions to represent sums as a tagged union.
+\item encoding products as an indexed union.
+\item exploiting argument form of types to represent unions.
+\item removing syntactic sugar we introduced, such as the \arb{} operator that
+  represents an arbitrary value of a given type.
+\end{enumerate}
+
+We will give two running examples throughout, both with regards to the binary
+tree type \(\mu X. (\nat \to \nat) + X \times X\), with leaves labelled by
+functions natural to natural. In our first example we construct a balanced
+binary tree of depth \(n + 1\), with leaves filled by \systemtinline{f}:
+\begin{listing}[H]
+\begin{systemt}
+let balanced n f = primrec n with
+  Zero     => roll (Leaf f)
+| Suc tree => roll (Branch (tree, tree))
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
+
+Our other example composes the leaves of the tree into a single function,
+starting by applying the right-most leaf to the input value:
+\begin{listing}[H]
+\begin{systemt}
+let compose tree = foldmatch tree with
+  Leaf f        => f
+| Branch (f, g) => fun x => f (g x)
+\end{systemt}
+\end{listing}
+
+\TODO{
+  \begin{itemize}
+    \item state that the initial type of roll makes it hard to encode
+    \item explain that there could be an arbitrary number of recursive arguments
+      scattered in a term
+    \item describe that collecting them into one location makes future encoding
+      steps easier
+    \item justify why I add lists as a built-in type former
+    \item describe the strength function, the key step in this phase
+    \item state it is defined by induction on the outer functor
+  \end{itemize}
+}
+
+\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
+    \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
+    \item justify the max operator
+    \item justify the head operator
+    \item justify the snoc operator
+    \item justify the arb operator
+  \end{itemize}
+}
+
+\TODO{
+  \begin{itemize}
+    \item state that we encode lists using their eliminators
+    \item explain why a list is a pair of length and index function
+    \item give the encoding of cons
+    \item give the encoding of snoc
+    \item give the encoding of max
+    \item give the encoding of head
+  \end{itemize}
+}
+
+\TODO{
+  \begin{itemize}
+    \item state that we encode sums as tagged C-style unions
+    \item explain the operations and equations of unions
+    \item justify why sums are tagged unions
+    \item justify adding union types
+    \item justify the case operator on naturals
+  \end{itemize}
+}
+
+\TODO{
+  \begin{itemize}
+    \item state that we encode products as functions from naturals to unions
+    \item explain that products are heterogenous vectors
+    \item justify implementing products as homogenous functional vectors
+  \end{itemize}
+}
+
+\TODO{
+  \begin{itemize}
+    \item state that we encode unions as functions with possibly unused
+      arguments
+    \item define the union on types in argument form
+    \item define the put operator
+    \item define the get operator
+  \end{itemize}
+}
+
+\TODO{
+  \begin{itemize}
+    \item state that we desugar other operators last
+    \item define desugaring of arb
+    \item define desugaring of case
+    \item define desugaring of map
+    \item define desugaring of let
+  \end{itemize}
+}
+
+\end{document}