\documentclass[../main.tex]{subfiles}

\begin{document}
\section{System T}%
\label{sec:systemt}

System~T is a simply-typed lambda calculus. Its 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{\Gamma}[T]{t}{A}\) means that \(t\) is System~T term of type
\(A\) in context \(\Gamma\). \Cref{fig:syst-eq} gives the equational
theory. We have beta- and eta-equality of functions and beta-reduction
of natural numbers.

\begin{figure}
  \[
  \begin{array}{ccc}
    \begin{prooftree}
      \hypo{x : A \in \Gamma}
      \infer1{\judgement{\Gamma}[T]{x}{A}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement{\Gamma, x : A}[T]{t}{B}}
      \infer1{\judgement{\Gamma}[T]{\lambda x. t}{A \to B}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement{\Gamma}[T]{f}{A \to B}}
      \hypo{\judgement{\Gamma}[T]{t}{A}}
      \infer2{\judgement{\Gamma}[T]{f~t}{B}}
    \end{prooftree}
    \\\\
    \begin{prooftree}
      \infer0{\judgement{\Gamma}[T]{\zero}{\nat}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement{\Gamma}[T]{t}{\nat}}
      \infer1{\judgement{\Gamma}[T]{\suc~t}{\nat}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement{\Gamma}[T]{t}{\nat}}
      \hypo{\judgement{\Gamma}[T]{u}{A}}
      \hypo{\judgement{\Gamma, x : A}[T]{v}{A}}
      \infer3{\judgement{\Gamma}[T]{\primrec{t}{u}{(x.v)}}{A}}
    \end{prooftree}
  \end{array}
  \]
  \caption{Typing judgements for System~T}\label{fig:syst-typing}
\end{figure}

\begin{figure}
  \begin{align*}
    (\lambda x. t)~u &= \sub{t}{x/u} \\
    \lambda x. t~x &= t \qquad (x \notin t)\\
    \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}\label{fig:syst-eq}
\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}~\cites{dialectica?}{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. \textcite{syst-sn} proves all System~T
terms are strongly normalising.

\subsection{Strategies for Encoding Inductive Types}%
\label{subsec:encoding-strategies}

Inductive data types as found in ML are a useful programming
abstraction that is missing from System~T. If we are to effectively
encode a data type, there are three fundamental operations we need to
account for:
\begin{enumerate}
  \item constructors to form values of the data type;
  \item folding to fully consume a value;
  \item pattern matching to support iterating on multiple values simultaneously
\end{enumerate}
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
\systemtinline{t} to see if it is also a leaf. If
\systemtinline{tree1} is instead a branch, the \foldkw{} provides
equality predicates \systemtinline{l} and \systemtinline{r} for its
two subtrees by the induction principal. We again pattern match on the
other tree and when it is also a branch we test equality recursively
with the predicates.

\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 data types within System~T. We judge each encoding
on:
\begin{itemize}
  \item if it can encode inductive types with higher-order data such
    as functions;
  \item if it is a local, simply-typed transformation that does not
    require polymorphism or a global program analysis; and
  \item how easy it is to hand write the three fundamental operations.
\end{itemize}
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 two columns assesses whether a strategy works for
    higher-order types and is a local, simply-typed transformation. The
    remainder indicate whether it is ``easy'' (\ding{51}) or possible
    (\ding{81}) to hand write the constructors, fold and pattern matching
    respectively.}\label{tbl:encodings}
  \begin{tabular}{lccccc}
    \toprule
    Strategy & Higher Order & Local & Constructors & Fold & Pattern Match \\
    \midrule
    G\"odel & \ding{55} & \ding{51} & \ding{51} & \ding{81} & \ding{51} \\
    Church & \ding{51} & \ding{55} & \ding{51} & \ding{51} & \ding{81} \\
    Eliminator & \ding{51} & \ding{51} & \ding{51} & \ding{55} & \ding{55} \\
    Heap & \ding{51} & \ding{51} & \ding{81} & \ding{81} & \ding{51} \\
    \bottomrule
  \end{tabular}
\end{table}

\subsubsection*{G\"odel Encodings}

G\"odel encodings~\cite{dialectica?} represent data types as natural
numbers. It is well-known that there are pairing functions, invertible
functions from \(\mathbb{N} \times \mathbb{N}\) to \(\mathbb{N}\), that are primitive
recursive~\cite{pairing}. We can use pairing 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*}
One can pattern match on G\"odel encodings by unpairing a value to
split it back into the tag and payload.

A major limitation of G\"odel encodings is that they cannot represent
higher-order data such as functions. G\"odel encodings by definition
encode data as natural numbers. We cannot encode arbitrary functions
as naturals, even in simple models such as \(\mathsf{Set}\). If we
restrict ourselves to representable functions, \textcite{bauer} proves
we cannot recover a function from its syntax.

Another difficulty with G\"odel encodings is implementing the fold
operation. We need our chosen pairing function to be increasing so
that values are ``large enough'' to iterate
over. \Cref{fig:godel-fold} shows how to encode fold over binary
trees. We use primitive recursion to construct the function \(go\). At
the \(n\)th recursive step, \(go\) will correctly fold any value
strictly less than \(n\). For the base case, any result is vacuously
correct, so \(go\) returns an arbitrary value. To construct the next
iteration of \(go\), we pattern match on the input value. As our
chosen pairing function is increasing, we can pass any inductive
components to the previous iteration of \(go\). We then apply the
appropriate branch for the constructor we have. As the target \(t\) is
less than \(\suc~t\), we can pass the target to \(go\) to compute the
fold.

\begin{figure}
  \[
    \dofoldmatch*[t]{t}{
      \mathsf{leaf}(n). f(n);
      \mathsf{branch}(x, y). g(x, y)
    } \coloneq
    \dolet{go}*{
      \doprimrec*{\suc~t}{\arb}{h}{
        \lambda i. \domatch*{i}{
          \mathsf{leaf}(n). f(n);
          \mathsf{branch}(l, r). g(h(l), h(r))}}
    }*{go~t}
  \]
  \caption{The G\"odel encoding of \foldkw{} for binary
    trees.}\label{fig:godel-fold}
\end{figure}

\subsubsection*{Church Encodings}

Typically used in untyped settings, Church encodings represent data by
their fold operation~\cite{church}. For example binary trees are
Church encoded by the type \(T = \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 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}
  \[
    \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 results of
eliminators. With our sum and depth example, we encode the
constructors by
\begin{align*}
  \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*}
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 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}
    \item create box-and-pointer diagram
  \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. 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}{
  \mathsf{leaf}(n).      f(n);
  \mathsf{branch}(x, y). g(x, y)
} \coloneq
\dolet
  {\tuple{depth, root, heap}}{t}
  {go}*{
    \doprimrec*{depth}
      {\arb{}}
      {h}{\lambda i.
        \domatch*{heap~i}{
          \mathsf{Left}(n).     f(n);
          \mathsf{Right}(j, k). g(h~i, h~j)}}}
  *{go~root}
\]

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}
