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. 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 some of their
(contravariant) consumers~\cite{eliminator-enc}. 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. The encoded type contains no information about which
constructor was used to construct a value. Thus we are free to add new
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 and extend the weaknesses of Church
encodings. Defining an arbitrary fold requires polymorphism in
general. 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.

A notable exception to this general trend is lists. We can encode a
list as a pair of its length and its index function, returning the
element at a given position. From these two eliminators, we can
reconstruct both folds and pattern matching.

\subsubsection*{Heap Encodings}

This encoding strategy is a crude approximation of a heap of
memory~\cite{heap}. 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 depicted 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.

\begin{figure}
  \caption{\TODO{create box-and-pointer diagram}}%
\label{fig:box-pointer:tree}\label{fig:box-pointer:heap}
\end{figure}

The recursive depth is essential for the fold operation. We give an
example in \cref{fig:heap-fold}. The \(results\) function constructs 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, \(results\) returns 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 \(results\) looks up the constructor and payload in the heap. It
uses the induction hypothesis to replace inductive components with
their final values, and then applies the appropriate fold branch. We
retrieve the final value by looking up the root in \(results\).

\begin{figure}
  \[
  \dofoldmatch*{t}{
    \mathsf{leaf}(n).      f(n);
    \mathsf{branch}(x, y). g(x, y)
  } \coloneq
  \dolet
    {\tuple{depth, root, heap}}{t}
    {results}*{
      \doprimrec*{depth}
        {\arb{}}
        {h}{\lambda i.
          \domatch*{heap~i}{
            \mathsf{Left}(n).     f(n);
            \mathsf{Right}(j, k). g(h~i, h~j)}}}
    *{results~root}
  \]
  \caption{The heap encoding of fold for binary trees.}%
\label{fig:heap-fold}
\end{figure}

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 a part for the inductive component to recurse in to and a
part for the index within that component's heap. Pointers in payloads
in each inductive components' component's heap are then ``fixed up''
as appropriate. One also needs a special index to refer to the payload
of the new root. For instance with natural number indices, we can use
\zero{} for the root and \(\suc~\tuple{i, k}\) for index \(k\) in
inductive component \(i\).

\end{document}