From 4353f331b5ab4af157f576f54b1cc79dd08abb12 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 23 Apr 2025 15:59:22 +0100
Subject: Current state of affairs.

---
 sec/systemt.ltx | 330 ++++++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 249 insertions(+), 81 deletions(-)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 12b1ed2..7881396 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -4,32 +4,23 @@
 \section{System T}%
 \label{sec:systemt}
 
-G\"odel's System~T extends the simply-typed lambda calculus by adding natural
-numbers and the primitiver recursor. The type formers are \(\nat\) for natural
-numbers and arrows \(A \to B\) for functions.
-
-\Cref{fig:systemt-type} shows the typing rules for System~T terms. On top of the
-usual abstraction and application rules, we can construct unary natural numbers
-using the operators \(\zero\) and \(\suc\). Natural numbers are eliminated using
-the primitive recursor \primreckw. Given a base case, update function and target
-\(n\), the primitive recursor applies the update function to the target \(n\)
-times. We will abuse notation and treat the \(\suc\) and \primreckw operators as
-functions.
+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.
 
 \begin{figure}
   \[
   \begin{array}{ccc}
     \begin{prooftree}
-      \hypo{
-        x : A \in \Gamma
-        \vphantom{\judgement[T]{}{}{}} %% Spooky formatting phantom
-      }
+      \hypo{x : A \in \Gamma}
       \infer1{\judgement[T]{\Gamma}{x}{A}}
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement[T]{\Gamma, x \colon A}{t}{B}}
-      \infer1{\judgement[T]{\Gamma}{\lambda x.~t}{A \to B}}
+      \hypo{\judgement[T]{\Gamma, x : A}{t}{B}}
+      \infer1{\judgement[T]{\Gamma}{\lambda x. t}{A \to B}}
     \end{prooftree}
     &
     \begin{prooftree}
@@ -37,11 +28,9 @@ functions.
       \hypo{\judgement[T]{\Gamma}{t}{A}}
       \infer2{\judgement[T]{\Gamma}{f~t}{B}}
     \end{prooftree}
-    \\
-    \\
+    \\\\
     \begin{prooftree}
-      \hypo{\vphantom{\judgement[T]{}{}{}}} %% Spooky formatting phantom
-      \infer1{\judgement[T]{\Gamma}{\zero}{\nat}}
+      \infer0{\judgement[T]{\Gamma}{\zero}{\nat}}
     \end{prooftree}
     &
     \begin{prooftree}
@@ -50,81 +39,260 @@ functions.
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement[T]{\Gamma}{z}{A}}
-      \hypo{\judgement[T]{\Gamma}{s}{A \to A}}
       \hypo{\judgement[T]{\Gamma}{t}{\nat}}
-      \infer3{\judgement[T]{\Gamma}{\primrec{z}{s}{t}}{A}}
+      \hypo{\judgement[T]{\Gamma}{u}{A}}
+      \hypo{\judgement[T]{\Gamma, x : A}{v}{A}}
+      \infer3{\judgement[T]{\Gamma}{\primrec{t}{u}{(x.v)}}{A}}
     \end{prooftree}
   \end{array}
   \]
-  \caption{Typing judgements for System~T}%
-  \label{fig:systemt-type}
+  \caption{Typing judgements for System~T}\label{fig:syst-typing}
 \end{figure}
 
-The equational theory is defined in \cref{fig:systemt-eq}. We have the standard
-\(\beta\)-reduction for functions. When we apply the primitve recursor to target
-zero, we get the base case. When the recursor is applied to target \(\suc~t\),
-we apply the update function to the result of applying \primreckw{} recursively.
-An alternative theory would instead apply the update function directly to the
-base case instead of to the overall result of the recursion.  Whilst this has
-little impact for System~T (and operationally corresponds to tail recursion) the
-alternative rule does not generalise to the more complex recursive types found
-in \lang{}.
-
 \begin{figure}
   \begin{align*}
-    (\lambda x.~t)~u &= \sub{t}{x/u} &
-    \primrec{z}{s}{\zero} &= z &
-    \primrec{z}{s}{(\suc~t)} &= s~(\primrec{z}{x}{s}{t})
+    (\lambda x. t)~u &= \sub{t}{x/u} \\
+    \primrec{\zero}{u}{(x.v)} &= u \\
+    \primrec{(\suc~t)}{u}{(x.v)} &= \sub{v}{x/\primrec{t}{u}{(x.v)}}
   \end{align*}
-  \caption{Equational theory for System~T. \TODO{add eta for unions}}%
-  \label{fig:systemt-eq}
+  \caption{Equational theory for System~T}\label{fig:syst-eq}
 \end{figure}
 
-The primitive recursor is named as such because it generalises the first-order
-primitive recursive functions. For example, we can define addition as
-\[
-k + n = \primrec{n}{\suc}{k}.
-\]
-Despite its name, the primitive recursor can compute more than the primitive
-recursive functions. By exploiting the higher-order nature of System~T, one can
-define the Ackermann-P\'eter function~\cite{semantic-domain} as
+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.
+
+\subsection{Strategies for Encoding Inductive Types}%
+\label{subsec:encoding-strategies}
+
+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
+\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.
+
+\begin{listing}
+  \begin{systemt}
+  let equal tree1 tree2 =
+    let go = fold tree1 with
+      Leaf k => fun t => match t with
+        Leaf n     => k == n
+      | Branch _ _ => false
+    | Branch eql eqr => fun t => match t with
+        Leaf _     => false
+      | Branch l r => eql l && eqr r
+    in
+    go tree2
+  \end{systemt}
+  \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
+is a local, simply-typed transformation 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.
+
+\begin{table}
+  \caption{Comparison of encoding strategies for inductive types within
+    System~T. The first column assesses if the strategy is a local, simply-typed
+    transformation. The remainder indicate whether it is ``easy'' to hand write
+    the constructors, fold and pattern matching
+    respectively.}\label{tbl:encodings}
+  \begin{tabular}{lcccc}
+    \toprule
+    Strategy & Local & Constructors & Fold & Pattern Match \\
+    \midrule
+    G\"odel & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\
+    Church & \ding{55} & \ding{51} & \ding{51} & \ding{55} \\
+    Eliminator & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\
+    Heap & \ding{51} & \ding{55} & \ding{51} & \ding{51} \\
+    \bottomrule
+  \end{tabular}
+\end{table}
+
+\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
+\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.
 \[
-\lambda k, m.~\primrec{\suc}{(\lambda f.~\primrec{(\lambda n.~n)}{(\lambda g, n.~f~(g~n))})}{k}~m.
+  \dofoldmatch*[t]{t}{
+    \mathsf{leaf}(n). f(n);
+    \mathsf{branch}(x, y). g(x, y)
+  } \coloneq
+  \dolet{
+    go = \doprimrec*{t}{\arb}{h}{
+      \lambda i. \domatch*{i}{
+        \mathsf{leaf}(n). f(n);
+        \mathsf{branch}(l, r). g(h(l), h(r))}}
+  }*{go~t}
 \]
 
-Any countable set can be encoded by natural numbers. For inductively defined
-sets, such as lists or abstract syntax trees for programs, one can use a G\"odel
-encoding to represent values as natural numbers. This depends on a pairing
-function \(\pairingkw : \nat \to \nat \to \nat\) that is a (curried)
-bijection \(\nat \times \nat \to
-\nat\)~\cites{DiscoverEd:book/oc/Cantor52}{szudzik}. As some examples, we can
-encode lists of natural numbers as
+\subsubsection*{Church Encodings}
+
+Typically used in untyped settings, Church encodings represent data by their
+fold operation. For example binary trees are Church encoded by the type \(\forall A.
+(\nat \to A) \to (A \to A \to A) \to A\). The first argument describes how to deconstruct
+leaves, and the second applies the inductive step on branches. This encoding
+makes implementing fold trivial. Constructors for the inductive types are also
+simple to encode, as demonstrated by the following example:
+\begin{align*}
+  \mathsf{leaf}(n) &\coloneq \lambda l, b.~l~n
+  &
+  \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}
+
+\begin{figure}
+  \[
+    \domatch*[t]{t}{
+      \mathsf{leaf}(n).     f(n);
+      \mathsf{branch}(x,y). g(x, y)
+    } \coloneq
+    \dolet[t]{
+      \roll = \lambda x. \domatch*[t]{x}{
+        \mathsf{Left}(n).     \mathsf{leaf}(n);
+        \mathsf{Right}(x, y). \mathsf{branch}(x, y)
+      }
+    }{
+      x = \dofoldmatch*{t}{
+        \mathsf{leaf}(n).      \mathsf{Left}(n);
+        \mathsf{branch}(x, y). \mathsf{Right}(\roll~x, \roll~y)
+      }
+    }*{
+      \domatch*{x}{
+        \mathsf{Left}(n).     f(n);
+        \mathsf{Right}(x, y). g(x, y)
+      }
+    }
+  \]
+  \caption{How to perform pattern matching on binary trees for Church encodings.
+    We assume we have an encoding for sums with pattern matching.}\label{fig:church-pm}
+\end{figure}
+
+You may have noticed that this encoding included a type quantification---in
+general, one must use polymorphism to fully represent Church encodings. To avoid
+polymorphism requires a global analysis, replacing the polymorphic bound with a
+(hopefully) finite product of possible consumers.
+
+\subsubsection*{Eliminator Encodings}
+
+This encoding strategy generalises Church encodings. Rather than encoding
+inductive types by their folds, eliminator encodings represent inductive types
+as a product of all their (contravariant) consumers. For example, if we know the
+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
 \begin{align*}
-  \encode{\epsilon} &\coloneq \pairing{0}{0} &
-  \encode{n, l} &\coloneq \pairing{1}{(\pairing{n}{\encode{l}})} \\
-  \shortintertext{and System~T terms (using deBruijn indices) as}
-  \encode{x_i}               &\coloneq \pairing{0}{i} &
-  \encode{\zero}             &\coloneq \pairing{3}{0} \\
-  \encode{\lambda~t}         &\coloneq \pairing{1}{\encode{t}} &
-  \encode{\suc~t}            &\coloneq \pairing{4}{\encode{t}} \\
-  \encode{t~u}               &\coloneq \pairing{2}{(\pairing{\encode{t}}{\encode{u}})} &
-  \encode{\primrec{z}{s}{t}} &\coloneq
-    \pairing{5}{(\pairing{\encode{z}}{(\pairing{\encode{s}}{\encode{t}})})}.
+  \mathsf{leaf}(n) &\coloneq \tuple{n, 1}
+  &
+  \mathsf{branch}(x, y) &\coloneq \tuple{x.0 + y.0, \suc~(x.1 \sqcup y.1)}
 \end{align*}
-In general, each constructor has a unique tag and this is paired with an
-encoding for each subterm. We can analyse an encoded term by reverting the
-pairing function and inspecting the tag. For an invalid tag (for our encoding of
-lists this is anything greater than 2) we can return an arbitrary value.
-Performing recursion on G\"odel encodings is difficult, particularly for values
-with more than one recursive argument.
-
-An alternative encoding strategy uses functions to encode data. One example we
-have already given is our encoding of binary trees, from the introduction.
-Another functional encoding is to represent lists as functions \(\nat \to
-\nat\). Giving the function \zero{} will return the length of the list, and the
-values are 1-indexed. This strategy doesn't require a pairing function, but
-values no longer have a unique representation. For example, the functions
-\(\lambda n.~n + n\) and \(\lambda n. \zero\) both represent the empty list.
+using \(k \sqcup n\) to compute the maximum of two naturals. We can easily encode the
+specified eliminators too; simply take the corresponding projection from the
+product.
+
+Another benefit of eliminator encodings are that the constructors are
+extensible. As no information about exactly which constructor was used remains
+in the encoded type, we are free to add some interesting constructors. For
+example, we can add the constructor \(\mathsf{double}\) that doubles the value
+of each leaf:
+\[
+\mathsf{double}(x) \coloneq \tuple{2 \cdot x.0, x.1}
+\]
+
+Eliminator encodings inherit the weaknesses of Church encodings. Defining an
+arbitrary fold requires polymorphism. Pattern matching is also impossible in the
+general case. With our sum and depth example, we have no way of knowing whether
+the value representing a tree came from a leaf or branch as we deliberately
+forget this information.
+
+\subsubsection*{Heap Encodings}
+
+This encoding strategy is a crude approximation of a heap of memory. Given an
+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).
+
+
+%% This encoding strategy is a crude approximation of a heap of memory.
+%% Implementing this strategy requires choosing a (first-order) indexing type. Due
+%% to G\"odel encodings, \nat{} is sufficient. In \cref{subsec:encode-inductive} we
+%% use lists of naturals to better reflect the tree-like structure of inductive
+%% values.
+
+\TODO{
+  \begin{itemize}
+    \item describe with a box-and-pointer diagram
+    \item explain briefly how to fold and roll
+  \end{itemize}
+}
 
 \end{document}
-- 
cgit v1.2.3

