Revise System T.

1 files changed, 110 insertions, 96 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 8b3f173..d25bd22 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -4,11 +4,13 @@
 \section{System T}%
 \label{sec:systemt}
 
-System~T is a simply-typed lambda calculus. The types are naturals \nat{} and
-functions \(A \to B\), and on top of function abstraction and application, we
-have \zero{} and \suc{} for zero and successor, as well as \primreckw{}, the
-primitive recursor. \Cref{fig:syst-typing} shows the typing judgements and
-\cref{fig:syst-eq} the equational theory.
+System~T is a simply-typed lambda calculus. The types are naturals
+\nat{} and functions \(A \to B\). On top of the function abstraction and
+application operators, we have \zero{} and \suc{} for zero and
+successor, as well as \primreckw{}, the primitive
+recursor. \Cref{fig:syst-typing} shows the typing judgements, where
+\(\judgement[T]{\Gamma}{t}{A}\) means that \(t\) is System~T term of type
+\(A\) in context \(\Gamma\), and \cref{fig:syst-eq} the equational theory.
 
 \begin{figure}
   \[
@@ -59,15 +61,18 @@ primitive recursor. \Cref{fig:syst-typing} shows the typing judgements and
 \end{figure}
 
 Types in System~T are usually presented as binary trees, with branches
-representing arrows and leaves being \(\nat\). An alternative presentation is
-\emph{argument form}~\cite{DBLP:books/sp/LongleyN15}. Notice that all types can
-be written in the form \(A_1 \to \cdots \to A_n \to \nat\) for some unique list of argument
-types \(A_i\). We can therefore represent a type by its list of arguments. For
-example, the type \(\nat\) has argument form \(\epsilon\), and the type \(\nat \to \nat \to
-(\nat \to \nat) \to \nat\) has argument form \([\epsilon, \epsilon, [\epsilon]]\).
-
-Argument form makes it obvious that all types in System~T are inhabited. For
-example, we can use the constantly zero function as an arbitrary inhabitant.
+representing arrows and leaves being \(\nat\). An alternative
+presentation is \emph{argument
+form}~\cite{DBLP:books/sp/LongleyN15}. Notice that all types can be
+written in the form \(A_1 \to \cdots \to A_n \to \nat\) for some unique list of
+argument types \(A_i\). We can therefore represent a type by its list
+of arguments. For example, the type \(\nat\) has argument form \(\epsilon\)
+(the empty list), and the type \(\nat \to \nat \to (\nat \to \nat) \to \nat\)
+has argument form \([\epsilon, \epsilon, [\epsilon]]\).
+
+All System~T types are inhabited.\@ \nat{} is inhabited by zero, and
+any function type is inhabited when its codomain is inhabited by
+taking the constant function.
 
 \subsection{Strategies for Encoding Inductive Types}%
 \label{subsec:encoding-strategies}
@@ -76,20 +81,18 @@ Inductive types are a useful programming abstraction that is missing from
 System~T. If we are to effectively encode an inductive type, there are three
 operations we would like to use:
 \begin{enumerate}
-  \item constructors
-  \item folding
-  \item pattern matching
+  \item constructors to form values of an inductive type;
+  \item folding to fully consume an inductive value;
+  \item pattern matching to support iterating on multiple values simultaneously
 \end{enumerate}
-We need constructors else we cannot write values of the inductive type. We need
-folding so we can fully consume the inductive type in a total way. We need
-pattern matching so we can iterate over multiple values. As a concrete example,
-consider the pseudocode in \cref{lst:tree-eq} for comparing whether two binary
-trees are equal. We use a fold to create an equality predicate out of
-\systemtinline{tree1}. When \systemtinline{tree1} is a leaf, we pattern match on
-the other tree to see if it is also a leaf. If \systemtinline{tree1} is instead
-a branch, we obtain equality predicates for its two subtrees by its induction
-principal. We again pattern match on the other tree to see if it also a branch,
-and test equality recursively.
+As a concrete example, consider the pseudocode in \cref{lst:tree-eq}
+for comparing whether two binary trees are equal. We use a fold to
+create an equality predicate out of \systemtinline{tree1}. When
+\systemtinline{tree1} is a leaf, we pattern match on the other tree to
+see if it is also a leaf. If \systemtinline{tree1} is instead a
+branch, we obtain equality predicates for its two subtrees by the
+induction principal. We again pattern match on the other tree and test
+equality recursively when it is also a branch.
 
 \begin{listing}
   \begin{systemt}
@@ -107,13 +110,14 @@ and test equality recursively.
   \caption{Pseudocode for determining equality of two binary trees.}\label{lst:tree-eq}
 \end{listing}
 
-In the remainder of the section we outline four different strategies for
-encoding inductive types within System~T. We judge each encoding on whether it
-can encode inductive types with higher-order data such as functions; is a local,
-simply-typed transformation that does not require polymorphism or a global
-program analysis; as well as how easy it is to hand write the three fundamental
-operators. As you can see from the summary in \cref{tbl:encodings}, each
-strategy is lacking in some regard.
+In the remainder of the section we outline four different strategies
+for encoding inductive types within System~T. We judge each encoding
+on: if it can encode inductive types with higher-order data such as
+functions; if it is a local, simply-typed transformation that does not
+require polymorphism or a global program analysis; how easy it is to
+hand write the three fundamental operators. As you can see from the
+summary in \cref{tbl:encodings}, each strategy is lacking in some
+regard.
 
 \begin{table}
   \caption{Comparison of encoding strategies for inductive types within
@@ -136,39 +140,43 @@ strategy is lacking in some regard.
 
 \subsubsection*{G\"odel Encodings}
 
-G\"odel encodings represent inductive data types as natural numbers. It is
-well-known that there are pairing functions, bijections from \(\mathbb{N} \times
-\mathbb{N}\) to \(\mathbb{N}\), that are primitive recursive. We can use these
-functions to encode inductive data types as pairs of tags and values. Writing
-\(\tuple{\cdot, \cdot}\) for the pairing function, we can encode the binary
-tree constructors as
+G\"odel encodings represent inductive data types as natural
+numbers. It is well-known that there are pairing functions, bijections
+from \(\mathbb{N} \times \mathbb{N}\) to \(\mathbb{N}\), that are primitive recursive. We can use
+these functions to encode inductive types as pairs of tags and
+payloads, such that every constructor has a unique tag. Writing
+\(\tuple{\cdot, \cdot}\) for a chosen pairing function, we can encode the
+binary tree constructors as
 \begin{align*}
   \mathsf{leaf}(n) &\coloneq \tuple{0, n} \\
   \mathsf{branch}(l, r) &\coloneq \tuple{1, \tuple{l, r}}.
 \end{align*}
-Pattern matching on G\"odel encodings is achieved by using the unpairing part of
-the bijection to determine the specific constructor and its payload.
-
-One major limitation of G\"odel encodings is that they cannot represent
-higher-order data such as functions. The defining trait of G\"odel encodings is
-that they represent data by natural numbers, and as function types cannot be
-encoded as naturals, we cannot encode functions. We also cannot use a syntactic
-representation of functions; \textcite{Squid:unpublished/Bauer17} proves there
-is no System~T term that can recover a function from its syntax.
-
-Another difficulty with G\"odel encodings is implementing the fold operation.
-We require our choice of pairing function to be monotonic so that an encoded
-value is ``large enough'' to iterate over. The fold with motive type \(A\) then
-proceeds with a primitive recursion over the successor of the natural
-representing the target with motive type \(\nat \to A\). The intent is that the
-\((n+1)\)-th stage of recursion will correctly fold a target with encoding
-\(n\). There are no expectations for the base case for the recursion, so we can
-use an arbitrary value. For the successor case, we use pattern matching to
-deconstruct the input encoded value into its constructor and payload. We can use
-the inductive argument to fold over recursive values in the payload, and as the
-pairing function is monotonic, these values must be smaller than the current
-case, so the resulting value is correct. We then apply the appropriate case for
-the fold. Below is the fold over binary trees.
+One can pattern match on G\"odel encodings by using the unpairing part of
+the bijection to split a value back into the tag and payload.
+
+One major limitation of G\"odel encodings is that they cannot
+represent higher-order data such as functions. The defining trait of
+G\"odel encodings is that they represent data by natural numbers. As
+function types cannot be encoded as naturals, we cannot encode
+functions. We also cannot use a syntactic representation of functions;
+\textcite{Squid:unpublished/Bauer17} proves there is no System~T term
+that can recover a function from its syntax.
+
+Another difficulty with G\"odel encodings is implementing the fold
+operation.  We require our chosen pairing function to be monotonic so
+that an inductive value is ``large enough'' to iterate over.  To fold
+a target into the motive type \(A\), we use primitive recursion to
+construct a function from encodings into \(A\).  The intent is that
+the \((n+1)\)-th stage of recursion will correctly fold a target with
+encoding \(n\). There are no expectations for the base case for the
+recursion, so we can use an arbitrary value. For the successor case,
+we use pattern matching to deconstruct the function input into its tag
+and payload. We can use the induction hypothesis to fold over
+inductive components in the payload. Using the induction hypothesis
+gives a correct value, as a monotonic pairing function ensures each
+inductive component is smaller than the function input we are
+currently working on. We then apply the appropriate branch for the
+constructor we have. Below is the fold over binary trees.
 \[
   \dofoldmatch*[t]{t}{
     \mathsf{leaf}(n). f(n);
@@ -196,12 +204,13 @@ simple to encode, as demonstrated by the following example:
   \mathsf{branch}(x, y) &\coloneq \lambda l, b.~b~(x~l~b)~(y~l~b)
 \end{align*}
 
-Whilst Church encodings are great for representing folds and constructors,
-pattern matching becomes more challenging. The most general strategy is to use
-the fold to recover a sum over the possible constructors, and then eliminate
-this using the clauses of the pattern match. For example, we would fold a binary
-tree into the sum \(\nat + T \times T\), representing leaves and branches
-respectively, and then case split on this sum. We detail this in \cref{fig:church-pm}
+Whilst Church encodings are great for representing folds and
+constructors, pattern matching becomes more challenging. The most
+general strategy is to use the fold to recover a sum over the possible
+constructors, and then eliminate this using the branches of the
+pattern match. For example, we would fold a binary tree into the sum
+\(\nat + T \times T\), representing leaves and branches respectively, and
+then pattern match on this sum. We detail this in \cref{fig:church-pm}
 
 \begin{figure}
   \[
@@ -241,8 +250,9 @@ only operations we will perform on a binary tree are finding the sum of all
 leaves and the depth of the tree. We can encode the binary tree as a pair \(\nat
 \times \nat\), where the first value is the sum and the second is the depth.
 
-In this encoding, the constructors eagerly compute the eliminated values. With
-our sum and depth example, we encode the constructors by
+In this encoding, the constructors eagerly compute the results of
+eliminators. With our sum and depth example, we encode the
+constructors by
 \begin{align*}
   \mathsf{leaf}(n) &\coloneq \tuple{n, 1}
   &
@@ -274,16 +284,19 @@ indexing type \(I\), an inductive type is a triple of a \emph{recursive depth},
 a \emph{root index}, and an \(I\)-indexed \emph{heap} of values. Instead of
 storing recursive values ``in-line'', one stores an index to its place in the heap.
 
-Consider the binary tree \(\mathsf{branch}(\mathsf{branch}(\mathsf{leaf}(1),
-\mathsf{leaf}(2)), \mathsf{branch}(\mathsf{leaf}(3),
-\mathsf{branch}(\mathsf{leaf}(4), \mathsf{leaf}(5))))\), depicted
-diagramatically in \cref{fig:box-pointer:tree}. The recursive depth of the tree
-is three, as there are at most three nested constructors (e.g.\ the path from
-root to the value four). \Cref{fig:box-pointer:heap} gives a representation of
-the heap used to store this tree. Each constructor has its own place in the
-heap. Leaves store the value of the leaf; branches store the indices of the two
-children. Like Church encodings, this encoding relies on having an encoding for
-sums in order to store the data for different constructors within a single type.
+Consider the binary tree
+\(\mathsf{branch}(\mathsf{branch}(\mathsf{leaf}(1), \mathsf{leaf}(2)),
+\mathsf{branch}(\mathsf{leaf}(3), \mathsf{branch}(\mathsf{leaf}(4),
+\mathsf{leaf}(5))))\), depicted diagramatically in
+\cref{fig:box-pointer:tree}. The recursive depth of the tree is four,
+as there are at most four nested constructors (e.g.\ the path from
+root to the value five). \Cref{fig:box-pointer:heap} gives a
+representation of the heap used to store this tree. Each constructor
+has its own place in the heap. Leaves store the value of the leaf;
+branches store the indices of the two inductive components. Like
+Church encodings, this encoding relies on having an encoding for sums
+in order to store the data for different constructors within a single
+type.
 
 \TODO{
   \begin{itemize}
@@ -291,16 +304,16 @@ sums in order to store the data for different constructors within a single type.
   \end{itemize}
 }
 
-The recursive depth is essential for the fold operation. We iteratively
-construct a heap of values; the recursive depth is an upper bound on the number
-of steps it takes to converge on the ``true'' result of the fold. For recursive
-depth zero, we return an arbitrary value at each index, and as no inductive
-value is made from applying zero constructors, we have no soundness obligations.
-It is possible to return an arbitrary value as all System~T types are inhabited.
-For the successor case, at any given index we look up the constructor and
-associated data in the heap. We use the recursively-constructed return heap to
-replace inductive arguments with suitable values, and then apply the appropriate
-fold operation.
+The recursive depth is essential for the fold operation. We
+iteratively construct a heap of values; the recursive depth is an
+upper bound on the number of steps it takes to converge on the
+``true'' result of the fold. For recursive depth zero, we return an
+arbitrary value at each index. As no inductive value is made from
+applying zero constructors, we have no soundness obligations. For the
+successor case, at any given index we look up the constructor and
+payload in the heap. We use the induction hypothesis to replace
+inductive components with their final values, and then apply the
+appropriate fold branch.
 
 \[
 \dofoldmatch*{t}{
@@ -319,10 +332,11 @@ fold operation.
   *{go~root}
 \]
 
-\TODO{
-  \begin{itemize}
-    \item explain how to roll
-  \end{itemize}
-}
+Roll is harder to encode as it involves merging several heaps into
+one. The basic idea is that the indices for the new heap have to
+contain both which inductive component to recurse in to and the index
+within that component's heap. Pointers in payloads in the component's
+heap are then ``fixed up'' as appropriate. One also needs a special
+index to refer to the payload of the new root.
 
 \end{document}