path: root/sec/systemt.ltx

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

\begin{document}
\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.

\begin{figure}
  \[
  \begin{array}{ccc}
    \begin{prooftree}
      \hypo{x : A \in \Gamma}
      \infer1{\judgement[T]{\Gamma}{x}{A}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement[T]{\Gamma, x : A}{t}{B}}
      \infer1{\judgement[T]{\Gamma}{\lambda x. t}{A \to B}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement[T]{\Gamma}{f}{A \to B}}
      \hypo{\judgement[T]{\Gamma}{t}{A}}
      \infer2{\judgement[T]{\Gamma}{f~t}{B}}
    \end{prooftree}
    \\\\
    \begin{prooftree}
      \infer0{\judgement[T]{\Gamma}{\zero}{\nat}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement[T]{\Gamma}{t}{\nat}}
      \infer1{\judgement[T]{\Gamma}{\suc~t}{\nat}}
    \end{prooftree}
    &
    \begin{prooftree}
      \hypo{\judgement[T]{\Gamma}{t}{\nat}}
      \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:syst-typing}
\end{figure}

\begin{figure}
  \begin{align*}
    (\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}\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}~\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.
\[
  \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}
\]

\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*}
  \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 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.

\TODO{
  \begin{itemize}
    \item create box-and-pointer diagram
    \item explain briefly how to fold and roll
  \end{itemize}
}

\end{document}