Finish revisions.

1 files changed, 133 insertions, 119 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 7bfa1cf..fe94f2e 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -1,7 +1,7 @@
 \documentclass[../main.tex]{subfiles}
 
 \begin{document}
-\section{Encoding Artist}%
+\section{Encoding Artyst}%
 \label{sec:embedding}
 
 \TODO{
@@ -10,27 +10,29 @@
   \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:
+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 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
+\item changing the \roll{} operator so that all inductive components
   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 inductive types using a list-indexed heap.
+\item encoding lists using eliminators.
+\item introducing unions to encode sums as a tagged union.
 \item encoding products as an indexed union.
-\item exploiting argument form of types to represent unions.
+\item encoding unnions of System~T types.
 \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}:
+We will give two running examples throughout, both with regards to the
+binary tree type \(\mu X. (\nat \to \nat) + X \times X\), where leaves labelled
+by functions from natural to natural. In our first example we
+construct a balanced binary tree of depth \(n + 1\), with leaves
+filled by \systemtinline{f}. This will demonstrate how we encode
+constructors for inductive types.
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
@@ -40,8 +42,9 @@ let balanced n f = primrec n with
 \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:
+Our other example composes the leaves of a tree into a single function,
+starting by applying the right-most leaf to the input value. This will
+show how we encode destructors for inductive types.
 \begin{listing}[H]
 \begin{systemt}
 let compose tree = foldmatch tree with
@@ -53,16 +56,19 @@ let compose tree = foldmatch tree with
 \subsection{Phase 1: Simplifying Roll}%
 \label{subsec:simplify-roll}
 
-Recall the typing judgement for \roll{} in \cref{fig:lang-ty}. The premise has
-type \(\sub{A}{X/\mu X. A}\). One consequence of the use of substitution is that
-inductive values can appear scattered throughout a term of this type. Take the
-inductive type \(\mu X. (1 + \nat \times X + \mu Y. 1 + X \times Y) \times (1 + X)\). A term of
-this type can have any number of inductive values, located in distant parts of
-the term.
-
-Collecting all the inductive values into one location will make future encoding
-steps much easier. We enforce this by removing the \roll{} operator and adding
-the \roll*{} operator, which has the following type derivation:
+Recall the typing judgement for \roll{} in \cref{fig:lang-ty}. The
+argument has type \(\sub{A}{X/\mu X. A}\). One consequence of the use of
+substitution is that inductive components can appear scattered
+throughout a vessel of this type. Take the inductive type \(\mu
+X. \lgroup (1 + \nat \times X + \mu Y. (1 + X \times Y)) \times (1 + X) \rgroup\). The
+inductive parameter \(X\) appers in three seperate locations,
+including within another inductive type. A vessel of this shape could
+have any number of inductive components.
+
+Collecting all the inductive components into one location will make
+future encoding steps much easier. We enforce this by removing the
+\roll{} operator and adding the \roll*{} operator, which has the
+following type derivation:
 \[
 \begin{prooftree}
   \hypo{\judgement{\Gamma}{t}{\mathsf{List}~(\mu X.A)}}
@@ -70,38 +76,60 @@ the \roll*{} operator, which has the following type derivation:
   \infer2{\judgement{\Gamma}{\roll*~t~u}{\mu X. A}}
 \end{prooftree}
 \]
-Rather than include the inductive values within the term to roll, they are
-instead gathered into an external list. The places that contained inductive
-values in the rolled term now contain indices into the list. The new operator
-satisfies the following equation:
+Rather than including the inductive components within the argument of
+\roll{}, they are instead gathered into an external list. The vessel
+\(u\) now contains pointers to the inductive components within
+\(t\). The new operator satisfies the following equation:
 \[
 \dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u}
 \]
 
-\TODO{justify why I add lists as a built-in type former}
-
-To encode \roll{} into \roll*{} we require a function that traverses a term of
-type \(\sub{A}{X/\mu X. A}\) and collects all inductive values into a single list.
-We can extend a list with a single value and return the index of that value with
-the writer monad~\cite{writer}: \(\mathsf{extend} : A \to \mathsf{List}~A \to
-\mathsf{List}~A \times \nat\). By using the \mapkw{} operator we can replace all
-inductive values in a term \(\sub{A}{X/\mu X. A}\) with accumulator functions
-\(\sub{A}{X/\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times \nat}\). The
-non-trivial step is ``distributing'' the writer monad with the substitution to
-obtain a value of type \(\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times
-\sub{A}{X/\nat}\). We can apply this function to the empty list to obtain the
-arguments for \roll*{}.
-
-Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X \in
-\Psi\), a type environment \(\alpha\) and a type \(S\), we have a term
-\(\mathsf{distrib}\) defined in phase-one \lang{} of type
+We require a few operations on lists to compute this transformation:
+\(\mathsf{nil}\) representing the empty list; \(\mathsf{cons}\) for
+adding an element to the head of a list; \(\mathsf{length}\) to
+compute a list's length; and \(\mathsf{index}\) to retrieve a value
+from a list by position. We give the four equations these operators
+satisfy below. Note that whilst this encoding phase does not strictly
+require \(\mathsf{index}\), it is both necessary to describe the
+equational theory and will be used in the next phase.
+\begin{align*}
+\mathsf{length}~\mathsf{nil} &= \zero &
+\mathsf{index}~(\mathsf{cons}~t~u)~\zero &= t \\
+\mathsf{length}~(\mathsf{cons}~t~u) &= \suc~(\mathsf{length}~u) &
+\mathsf{index}~(\mathsf{cons}~t~u)~(\suc~n) &= \mathsf{index}~u~n
+\end{align*}
+
+To encode \roll{} into \roll*{} we require a function that traverses a
+value of type \(\sub{A}{X/\mu X. A}\) and collects all inductive
+components into a single list.  We can extend a list with a single
+value and return the index of that value with the function
+\(\mathsf{extend} : A \to \mathsf{List}~A \to \mathsf{List}~A \times \nat\)
+defined by \(\mathsf{extend}~a~t = \tuple{\mathsf{cons}~a~t,
+  \mathsf{length}~t}\). By using the \mapkw{} pseudo-operator we can
+replace all inductive components in a vessel \(\sub{A}{X/\mu X. A}\)
+with accumulator functions \(\sub{A}{X/\mathsf{List}~(\mu X. A) \to
+  \mathsf{List}~(\mu X. A) \times \nat}\). The non-trivial step is
+``distributing'' the accumulator with the substitution to obtain a
+value of type \(\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times
+\sub{A}{X/\nat}\). We can apply this function to the empty list to
+obtain the arguments for \roll*{}.
+
+Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type
+variable \(X \in \Psi\), a type environment \(\alpha\) and a type \(S\), we
+define a term \(\mathsf{distrib}\) of type
 \[
 \submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha}
 \]
-that calls each accumulator within \(A\) in sequence. The definition is by
-induction on the well-formedness derivation. At the end of this phase, the
-\systemtinline{compose} example is unchanged. The \systemtinline{balanced}
-example reduces to:
+that calls each accumulator within \(A\) in sequence.  The definition
+is by induction on the well-formedness derivation of \(A\). The
+details of the definition are in \cref{M-sec:distrib}.
+
+At the end of this phase, the \systemtinline{compose} example is
+unchanged. The \systemtinline{balanced} example reduces to the below
+code. Notice how the \suc{} branch uses the same variable
+\systemtinline{tree} in two different positions in the
+list. Optimising this encoding step to remove syntactic or semantic
+duplicates is left as future work.
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
@@ -115,10 +143,10 @@ let balanced n f = primrec n with
 \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.
+\(\mathsf{List}~\nat\)-indexed heap, but use naturals as pointers. The
+idea is that the heap index describes the path taken through the term
+to reach a particular entry, 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
@@ -133,10 +161,10 @@ Unlike the description of the heap encoding in
 and pointers. We use \(\mathsf{List}~\nat\) as the index type,
 representing a path through the term. We use the empty list to
 indicate the root of the inductive value. Otherwise, the head of the
-list selects which child to recurse into and the tail the path with
-this root. Instead of eagerly computing paths within the heap, we
-compute new paths lazily. The only necessary value to store is the
-index of the given child.
+list selects which child to recurse into and the tail of the path
+within this component. Instead of eagerly computing paths within the
+heap, we compute new paths lazily. This simplifies the \roll*{}
+operation as we do not need to fixup the entire heap.
 
 \begin{figure}
   \begin{align*}
@@ -156,17 +184,16 @@ index of the given child.
 \end{figure}
 
 More formally, we encode the type \(\mu X. A\) as \(\nat \times
-(\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
-We present the encoding of \roll*{} and \foldkw{} in
-\cref{fig:phase-2-encode}. We add four new operators for working with
-lists:
+(\mathsf{List}~\nat \to \sub{A}{X/\nat})\). We present the encoding of
+\roll*{} and \foldkw{} in \cref{fig:phase-2-encode}. We add three new
+operators for working with lists:
 \begin{description}
   \item[\(\mathsf{max}\)] for calculating the maximum from a list,
     given a function converting values to naturals;
-  \item[\(\mathsf{snoc}\)] for appending a single item to the end of a
-    list;
-  \item[\(\mathsf{index}\)] for retrieving an item from a list;
-  \item[\(\mathsf{match}\)] for pattern matching on a list.
+  \item[\(\mathsf{snoc}\)] for appending a single item to the tail of
+    a list;
+  \item[\(\mathsf{match}\)] for pattern matching on a list as either
+    \(\mathsf{nil}\) or \(\mathsf{cons}\)
 \end{description}
 Computing the maximum value from a list is necessary to correctly
 determine the recursive depth to use when folding over an inductive
@@ -176,38 +203,21 @@ X)\) of countable trees. To compute the recursive depth, we need to
 compute the maximum of a countable sequence, which is impossible in
 general. Thus we cannot encode such infinite types.
 
-Adding the \(\mathsf{snoc}\) operator may at first seem
-counterproductive; we want to encode away inductive types and
-recursion, yet \(\mathsf{snoc}\) is naively a recursion over an
-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.
+We need the \(\mathsf{snoc}\) operation to find the indices of
+inductive components within the encoding of \foldkw{}. This is true
+even if we computed paths eagerly during \roll*{}; we need
+\(\mathsf{snoc}\) to fixup paths there instead.
 
 The final operator we add at this phase is \(\mathsf{match}\) on
-lists. We can derive this operation using \(\mathsf{length}\) and
-\(\mathsf{index}\). We can use these two operators along with
-primitive recursion to define a fold over lists. With a fold, we can
-implement pattern matching analagously to \unroll{}. We keep it as an
-operator as our encoding of lists in the next phase will make this
-more efficient.
+lists. We need this to determine whether a path is addressing the root
+entry or one of its inductive components.
 
 We now return to our examples. After some beta reduction we recover
 the following value for \systemtinline{balanced}:
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
-  Zero => (1, fun xs =>
+  Zero => (Suc (max (fun (d, h) => d) []), fun xs =>
     match xs with
       []      => Leaf f
     | x :: xs => snd (index [] x) xs)
@@ -275,9 +285,7 @@ list and the second is the index function. We will justify using these
 eliminators by giving an encoding for each operator. Starting with the
 constructors, we can encode \(\mathsf{nil}\) by the pair \(\tuple{0,
   \arb}\). The empty list has length zero, and as there are no valid
-indices, we can give an arbitrary indexing function. Recall that all
-System~T types are inhabited which allows us to construct this
-arbitrary value.
+indices, we can give an arbitrary indexing function.
 
 We encode \(\mathsf{cons}~t~u\), adding element \(t\) to the head of
 the list \(u\), by
@@ -292,17 +300,17 @@ The length of our new list is one larger that
 the tail. To lookup a value, we first test whether the index is
 zero. If it is, we return the new head directly. Otherwise, we
 decrement the index and lookup its value in the tail. The encoding of
-\(\mathsf{if}\) and equality is standard~\cref{if+equals}.
+\(\mathsf{if}\) and equality is standard~\cite{if+equals}.
 
 The encoding of \(\mathsf{snoc}~t~u\), adding element \(u\) to the
-tail of the list \(t\), is encoded similarly:
+tail of the list \(t\), is similar:
 \[
 \tuple{
   \suc~t.0,
   \lambda x.\mathsf{if}~x = t.0~\mathsf{then}~u~\mathsf{else}~t.1~x
 }
 \]
-The new list is also one item longer that the old list. When looking
+The new list is again one item longer that the old list. When looking
 up an item, we first check if the index is the last in the list. If it
 is, we return the element we are adding to the tail. Otherwise, we
 lookup the index in the old list.
@@ -312,9 +320,9 @@ the list \(t\).
 \[\doprimrec{t.0}{\zero}{x}{(x.1 - f~x.0) + f~x.0}\]
 We compute the binary maximum by performing a truncated subtraction
 followed by an addition. These both have standard
-encodings~\cref{add+sub}. Note that we use the recursive value on the
-left of the subtraction so that a naive partial evaluator can reduce
-the maximum of a singleton list to a single value.
+encodings~\cref{add+sub}. Note that we use the inductive hypothesis on
+the left of the subtraction so that a naive partial evaluator can
+reduce the maximum of a singleton list to a single value.
 
 The final operator to encode is pattern matching. We achieve this by
 inspecting the length of the list to match.
@@ -330,7 +338,7 @@ inspecting the length of the list to match.
 The tricky part of this definition is computing the head and tail of a
 non-empty list. We retreive the head by calling the index function
 with index zero. The tail is one shorter that the initial list, and
-the index function is shifted by one too.
+the index function is shifted by one.
 
 We have shown that \(\mathsf{length}\) and \(\mathsf{index}\) are
 sufficient to produce an eliminator encoding for lists. We cannot add
@@ -391,15 +399,16 @@ let compose' (depth, heap) =
 
 In this phase we remove sums from the language by encoding them as
 tagged C-style unions, following the work of \textcite{oleg}. We
-encode the type \(\sum_i A_i\) by the pair \(\nat \times \bigsqcup_i A_i\), of
-a tag indicating which case we are in, and a union which can contain
-a value from any case.
+encode the type \(\sum_i A_i\) by the pair \(\nat \times \bigsqcup_i A_i\) of
+a tag indicating which case we are in, and a union which can contain a
+value from any case.
 
 Unions have two operators: \(\mathsf{inj}~i~t\) and
 \(\mathsf{prj}~t~i\) for injecting and projecting values at type
-\(A_i\) respectively. When the two types have the same index, unions
-have the beta reduction rule \(\mathsf{prj}~(\mathsf{inj}~i~t)~i =
-t\). If the two type indices are different then projection is stuck.
+\(A_i\) respectively. When the two operators have the same index,
+unions have the beta reduction rule
+\(\mathsf{prj}~(\mathsf{inj}~i~t)~i = t\). If the two indices are
+different then projection is stuck.
 
 We encode the injection into a sum \(\tuple{i, t}\) by the pair
 \(\tuple{i, \mathsf{inj}~i~t}\). We encode pattern matching
@@ -409,6 +418,8 @@ We encode the injection into a sum \(\tuple{i, t}\) by the pair
 to take. The pattern match on the right will be desugared into a
 sequence of equality tests in phase seven.
 
+\FIXME{these examples are hard to read}
+
 Our two examples reduce even further. We obtain the following for
 \systemtinline{balanced}:
 
@@ -487,15 +498,15 @@ let dupfirst t = fun x => match x with
 \subsection{Phase 6: Encoding Unions}%
 \label{subsec:unions}
 
-At this point, the only type former not present in System~T is the
-union type.\@ \textcite{oleg} gives an inductive encoding for binary
-unions. We instead use an encoding for unions derived from the
-argument form of types. Given we have a family of types \(A_i\) in
-argument form, their union is the concatenation \(A_1 \append A_2
-\append \cdots \append A_n\). To inject type \(A_k\) into the union, we
-ignore the function arguments for all the other type constructors. To
-project type \(A_k\) out of the union, we pass \(\mathsf{arb}\) to all
-the other arguments.
+At this point, the only type former we use that is not present in
+System~T is the union type.\@ \textcite{oleg} gives an inductive
+encoding for binary unions. We instead use an encoding for unions
+derived from the argument form of types. Given we have a family of
+types \(A_i\) in argument form, their union \(\bigsqcup_i A_i\) is the
+concatenation \(A_1 \append A_2 \append \cdots \append A_n\). To inject
+type \(A_k\) into the union, we ignore the function arguments for all
+the other types. To project type \(A_k\) out of the union, we pass
+\(\mathsf{arb}\) to all the other arguments.
 
 Using this argument-form union, we remove the need to perform
 induction on types, and only have to iterate over the number of types
@@ -504,7 +515,9 @@ union satisfies the required beta reduction rule. In exchange, our
 union encoding is neither idempotent nor commutative, and generally
 results in larger types than \posscite{oleg} encoding.
 
-The \systemtinline{dupfirst} example reduces to the following:
+The \systemtinline{dupfirst} example reduces to the below. If we
+instead used \posscite{oleg} encoding then the returned function would
+take only a single argument \systemtinline{x}.
 \begin{listing}[H]
 \begin{systemt}
 let dupfirst t = fun x => match x with
@@ -527,7 +540,8 @@ We encode case splitting on a number by a chain of equality tests. If
 all the tests fail, we will return an arbitrary value. We can
 construct an arbitrary value at any type by using the function that
 constantly returns zero. Let expressions are given their usual
-functional decoding.
+functional decoding as an abstraction applied immediately to an
+argument.
 
 The \systemtinline{dupfirst} example desugars into the following
 expression: