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

\begin{document}
\section{Encoding Artist}%
\label{sec:embedding}

\TODO{
  \begin{itemize}
    \item remind the reader why encoding into System~T is useful
  \end{itemize}
}

There are seven phases in the encoding process. In general, each phase removes a
specific type constructor until only naturals and function types remain.
Sometimes removing types requires introducing others; we will introduce lists of
naturals and C-style unions, which we will later need to remove. The full list
of seven phases are:
\begin{enumerate}
\item changing the type of the \roll{} operator so that all recursive arguments
  are collected together in a list.
\item using a list-indexed heap encoding to represent inductive types.
\item using an eliminator encoding to represent lists.
\item introducing unions to represent sums as a tagged union.
\item encoding products as an indexed union.
\item exploiting argument form of types to represent unions.
\item removing syntactic sugar we introduced, such as the \arb{} operator that
  represents an arbitrary value of a given type.
\end{enumerate}

We will give two running examples throughout, both with regards to the binary
tree type \(\mu X. (\nat \to \nat) + X \times X\), with leaves labelled by
functions natural to natural. In our first example we construct a balanced
binary tree of depth \(n + 1\), with leaves filled by \systemtinline{f}:
\begin{listing}[H]
\begin{systemt}
let balanced n f = primrec n with
  Zero     => roll (Leaf f)
| Suc tree => roll (Branch (tree, tree))
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

Our other example composes the leaves of the tree into a single function,
starting by applying the right-most leaf to the input value:
\begin{listing}[H]
\begin{systemt}
let compose tree = foldmatch tree with
  Leaf f        => f
| Branch (f, g) => fun x => f (g x)
\end{systemt}
\end{listing}

\subsection{Phase 1: Simplifying Roll}%
\label{subsec:simplify-roll}

Recall the typing judgement for \roll{} in \cref{fig:lang-ty}. The premise has
type \(\sub{A}{X/\mu X. A}\). One consequence of the use of substitution is that
inductive values can appear scattered throughout a term of this type. Take the
inductive type \(\mu X. (1 + \nat \times X + \mu Y. 1 + X \times Y) \times (1 + X)\). A term of
this type can have any number of inductive values, located in distant parts of
the term.

Collecting all the inductive values into one location will make future encoding
steps much easier. We enforce this by removing the \roll{} operator and adding
the \roll*{} operator, which has the following type derivation:
\[
\begin{prooftree}
  \hypo{\judgement{\Gamma}{t}{\mathsf{List}~(\mu X.A)}}
  \hypo{\judgement{\Gamma}{u}{\sub{A}{X/\nat}}}
  \infer2{\judgement{\Gamma}{\roll*~t~u}{\mu X. A}}
\end{prooftree}
\]
Rather than include the inductive values within the term to roll, they are
instead gathered into an external list. The places that contained inductive
values in the rolled term now contain indices into the list. The new operator
satisfies the following equation:
\[
\dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u}
\]

\TODO{justify why I add lists as a built-in type former}

To encode \roll{} into \roll*{} we require a function that traverses a term of
type \(\sub{A}{X/\mu X. A}\) and collects all inductive values into a single list.
We can extend a list with a single value and return the index of that value with
the writer monad~\cite{writer}: \(\mathsf{extend} : A \to \mathsf{List}~A \to
\mathsf{List}~A \times \nat\). By using the \mapkw{} operator we can replace all
inductive values in a term \(\sub{A}{X/\mu X. A}\) with accumulator functions
\(\sub{A}{X/\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times \nat}\). The
non-trivial step is ``distributing'' the writer monad with the substitution to
obtain a value of type \(\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times
\sub{A}{X/\nat}\). We can apply this function to the empty list to obtain the
arguments for \roll*{}.

Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X \in
\Psi\), a type environment \(\alpha\) and a type \(S\), we have a term
\(\mathsf{distrib}\) defined in phase-one \lang{} of type
\[
\submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha}
\]
that calls each accumulator within \(A\) in sequence. The definition is by
induction on the well-formedness derivation. At the end of this phase, the
\systemtinline{compose} example is unchanged. The \systemtinline{balanced}
example reduces to:
\begin{listing}[H]
\begin{systemt}
let balanced n f = primrec n with
  Zero     => roll2 []           (Leaf f)
| Suc tree => roll2 [tree, tree] (Branch (0, 1))
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

\subsection{Phase 2: Encoding Inductive Types}%
\label{subsec:inductive-types}

We use a modified heap encoding to encode regular types. We use a
\(\mathsf{List}~\nat\)-indexed heap, but keep the pointers within terms as
naturals. The idea is that the heap index describes the path taken through the
term to reach a particular point, whilst the pointers describe the next step
along the path.

We choose to use a heap encoding over another encoding strategy for the
following reasons. Firstly, inductive types in \lang{} can contain higher-order
data, such as our tree of functions, which prevents us from using G\"odel
encodings. Using a local translation makes writing the encoding easier, and as
System~T does not have polymorphism, we cannot use Church encodings. We need to
be able to write the fold operation, so we cannot use eliminator encodings. Thus
the only suitable encoding strategy is a heap encoding.

Unlike the description of the heap encoding in
\cref{M-subsec:heap-encoding} we do not use the same type for indices
and pointers. We use \(\mathsf{List}~\nat\) as the index type,
representing a path through the term. We use the empty list to
indicate the root of the inductive value. Otherwise, the head of the
list selects which child to recurse into and the tail the path with
this root. Instead of eagerly computing paths within the heap, we
compute new paths lazily. The only necessary value to store is the
index of the given child.

\begin{figure}
  \begin{align*}
    \roll*~ts~x &\coloneq \tuple*{
      \suc~(\mathsf{max}~(\mapkw~(\lambda t. t.0)~ts)),
      \lambda i. \domatch*{i}{
        \mathsf{nil}. x;
        \mathsf{cons}(i, j). {(\mathsf{index}~ts~i).1~j}}}
    \\
    \dofold{t}{x}{u} &\coloneq \dolet
      {go}*{\doprimrec*{t.0}
        {\arb}
        {r}{\lambda i. \sub{u}{x/\mapkw~(\lambda n. r~(\mathsf{snoc}~i~n))~(t.1~i)}}
      }*{go~\mathsf{nil}}
  \end{align*}
  \caption{Phase 2 encoding of the \roll*{} and \foldkw{} operators.}\label{fig:phase-2-encode}
\end{figure}

More formally, we encode the type \(\mu X. A\) as \(\nat \times
(\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
We present the encoding of \roll*{} and \foldkw{} in
\cref{fig:phase-2-encode}. We add four new operators for working with
lists:
\begin{description}
  \item[\(\mathsf{max}\)] for calculating the maximum from a list of
    naturals;
  \item[\(\mathsf{snoc}\)] for appending a single item to the end of a
    list;
  \item[\(\mathsf{index}\)] for retrieving an item from a list;
  \item[\(\mathsf{match}\)] for pattern matching on a list.
\end{description}
Computing the maximum value from a list is necessary to correctly
determine the recursive depth to use when folding over an inductive
value. It is also the primary reason why infinite inductive types are
forbidden. Take for example the inductive type \(\mu X. 1 + (\nat \to
X)\) of countable trees. To compute the recursive depth, we need to
compute the maximum of a countable sequence, which is impossible in
general. Thus we cannot encode such infinite types.

Adding the \(\mathsf{snoc}\) operator may at first seem
counterproductive; we want to encode away inductive types and
recursion, yet \(\mathsf{snoc}\) is naively a recursion over an
inductive type. Fortunately there exist encodings for lists such that
not only does \(\mathsf{snoc}\) avoid recursion, but it is also as
performant as cons.

Adding the \(\mathsf{index}\) operator should also cause no
issues. The biggest problem is deciding the result if the index is out
of bounds. Two approaches taken from other programming languages
include throwing an exception~\cites{exception} or returning an
optional value~\cites{optional}. System~T does not have exceptions as
a primitive, and returning an option doesn't help us consume the
value. Instead we return an arbitrary inhabitant of the type, possible
because all System~T types are inhabited. Regardless, one could prove
that our encoding never calls \(\mathsf{index}\) with an out-of-bounds
index.

The final operator we add at this phase is \(\mathsf{match}\) on
lists. We can derive this operation using \(\mathsf{length}\) and
\(\mathsf{index}\). We can use these two operators along with
primitive recursion to define a fold over lists. With a fold, we can
implement pattern matching analagously to \unroll{}. We keep it as an
operator as our encoding of lists in the next phase will make this
more efficient.

We now return to our examples. After some beta reduction we recover
the following value for \systemtinline{balanced}:
\begin{listing}[H]
\begin{systemt}
let balanced n f = primrec n with
  Zero => (1, fun xs =>
    match xs with
      []      => Leaf f
    | x :: xs => snd (index [] x) xs)
| Suc (depth, heap) => (Suc (max [depth, depth]), fun xs =>
    match xs with
      []      => Branch (0, 1)
    | x :: xs => snd (index [(depth, heap), (depth, heap)] x) xs)
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

And here is the updated value of \systemtinline{compose}:
\begin{listing}[H]
\begin{systemt}
let compose (depth, heap) =
  let go = primrec depth with
    Zero   => arb
  | Suc ih => fun index =>
    let x = map (fun x => ih (snoc index x)) (heap index) in
    match x with
      Leaf f        => f
    | Branch (f, g) => fun x => f (g x)
  in go []
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

\subsection{Phase 3: Encoding Lists}%
\label{subsec:lists}

This phase uses an eliminator encoding for lists. Recall we have the
following operators for lists: \(\mathsf{nil}\), \(\mathsf{cons}\),
\(\mathsf{length}\), \(\mathsf{index}\), \(\mathsf{max}\),
\(\mathsf{snoc}\) and \(\mathsf{match}\). We will encode all of these
operators using only the \(\mathsf{length}\) and \(\mathsf{index}\)
eliminators.

More formally, we encode the type \(\mathsf{List}~A\) by the type
\(\nat \times (\nat \to A)\), where the first component is the length of the
list and the second is the index function. We will justify using these
eliminators by giving an encoding for each operator. Starting with the
constructors, we can encode \(\mathsf{nil}\) by the pair \(\tuple{0,
  \arb}\). The empty list has length zero, and as there are no valid
indices, we can give an arbitrary indexing function. Recall that all
System~T types are inhabited which allows us to construct this
arbitrary value.

We encode \(\mathsf{cons}~t~u\), adding element \(t\) to the head of
the list \(u\), by
\[
\tuple{
  \suc~u.0,
  \lambda x.\mathsf{if}~x = \zero~
    \mathsf{then}~t~
    \mathsf{else}~u.0~(\mathsf{pred}~x)}
\]
The length of our new list is one larger that
the tail. To lookup a value, we first test whether the index is
zero. If it is, we return the new head directly. Otherwise, we
decrement the index and lookup its value in the tail. The encoding of
\(\mathsf{if}\) and equality is standard~\cref{if+equals}.

The encoding of \(\mathsf{snoc}~t~u\), adding element \(u\) to the
tail of the list \(t\), is encoded similarly:
\[
\tuple{
  \suc~t.0,
  \lambda x.\mathsf{if}~x = t.0~\mathsf{then}~u~\mathsf{else}~t.1~x
}
\]
The new list is also one item longer that the old list. When looking
up an item, we first check if the index is the last in the list. If it
is, we return the element we are adding to the tail. Otherwise, we
lookup the index in the old list.

We encode the \(\mathsf{max}\) operator by primitive recursion on the
length of the list \(t\).
\[\doprimrec{t.0}{\zero}{x}{(x.1 - x.0) + x.0}\]
We compute the maximum by performing a truncated subtraction followed
by an addition. These both have standard
encodings~\cref{add+sub}. Note that we use the recursive value on the
left of the subtraction so that a naive partial evaluator can reduce
the maximum of a singleton list to a single value.

The final operator to encode is pattern matching. We achieve this by
inspecting the length of the list to match.
\begin{multline*}
\domatch{t}{
  \mathsf{nil}. f;
  \mathsf{cons}(x, y). g
} \coloneq \\
\mathsf{if}~t.0 = \zero~\mathsf{then}~f~\mathsf{else}~\sub{g}{
  x/t.1~\zero, y/\tuple{\mathsf{pred}~t.0, \lambda i.~t.1~(\suc~i)}
}
\end{multline*}
The tricky part of this definition is computing the head and tail of a
non-empty list. We retreive the head by calling the index function
with index zero. The tail is one shorter that the initial list, and
the index function is shifted by one too.

We have shown that \(\mathsf{length}\) and \(\mathsf{index}\) are
sufficient to produce an eliminator encoding for lists. We cannot add
\(\mathsf{nil}\), \(\mathsf{cons}\) nor \(\mathsf{snoc}\) to the set
of eliminators, as these all construct lists. Similarly pattern
matching ``constructs'' the tail of a non-empty list. The only other
operator we could possibly add as an eliminator is
\(\mathsf{max}\). There are two main reasons we have not done
this. Firstly, \(\mathsf{max}\) is only defined on lists of naturals,
so we would end up with a non-uniform representation of
lists. Secondly, the maximum is only computed for a small number of
lists. In our running examples we compute the maximum only twice,
whereas we use lists thoughout. Carrying redundant data around for an
infrequent operation is inefficient and would complicate the encoding.

After phase three, our example for \systemtinline{balanced} beta
reduces to the following:
\begin{listing}[H]
\begin{systemt}
let balanced n f = primrec n with
  Zero => (1 , fun (length, idxs) =>
    if length == 0 then Leaf f else
      snd arb (length - 1, fun i => idxs (Suc i)))
| Suc (depth, heap) => (Suc ((depth - depth) + depth), fun (length, idxs) =>
    if length == 0 then Branch (0, 1) else
      let x = idxs 0 in
      let dh =
        if     x == 0 then (depth, heap) else
        if x - 1 == 0 then (depth, heap) else
          arb
      in snd dh (length - 1, fun i => idxs (Suc i)))
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

And \systemtinline{compose} reduces to:
\begin{listing}[H]
\begin{systemt}
let compose (depth, heap) =
  let go = primrec depth with
    Zero   => arb
  | Suc ih => fun (length, idxs) =>
    let x = map (fun x => ih (Suc length, fun i =>
                  if i == length then x else idxs i))
                (heap (length, idxs))
    in match x with
      Leaf f        => f
    | Branch (f, g) => fun x => f (g x)
  in go
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

\subsection{Phase 4: Encoding Sums}%
\label{subsec:sums}

In this phase we remove sums from the language by encoding them as
tagged C-style unions, following the work of \textcite{oleg}. We
encode the type \(\sum_i A_i\) by the pair \(\nat \times \bigsqcup_i A_i\), of
a tag indicating which case we are in, and a union which can contain
a value from any case.

Unions have two operators: \(\mathsf{inj}~i~t\) and
\(\mathsf{prj}~t~i\) for injecting and projecting values at type
\(A_i\) respectively. When the two types have the same index, unions
have the beta reduction rule \(\mathsf{prj}~(\mathsf{inj}~i~t)~i =
t\). If the two type indices are different then projection is stuck.

We encode the injection into a sum \(\tuple{i, t}\) by the pair
\(\tuple{i, \mathsf{inj}~i~t}\). We encode pattern matching
\((\casetm{t}{\tuple{i,x_i}}{t_i}{i})\) by the term \(
(\casetm{t.0}{i}{\sub{t_i}{x_i/\mathsf{prj}~t.1~i}}{i})
\) performing a pattern match over the tag to find the correct branch
to take. The pattern match on the right will be desugared into a
sequence of equality tests in phase seven.

\TODO{
  \begin{itemize}
    \item justify adding union types
    \item justify the case operator on naturals
  \end{itemize}
}

\subsection{Phase 5: Encoding Products}%
\label{subsec:products}

\TODO{
  \begin{itemize}
    \item state that we encode products as functions from naturals to unions
    \item explain that products are heterogenous vectors
    \item justify implementing products as homogenous functional vectors
  \end{itemize}
}

\subsection{Phase 6: Encoding Unions}%
\label{subsec:unions}

\TODO{
  \begin{itemize}
    \item state that we encode unions as functions with possibly unused
      arguments
    \item define the union on types in argument form
    \item define the put operator
    \item define the get operator
  \end{itemize}
}

\subsection{Phase 7: Desugaring}%
\label{subsec:desugar}

\TODO{
  \begin{itemize}
    \item state that we desugar other operators last
    \item define desugaring of arb
    \item define desugaring of case
    \item define desugaring of map
    \item define desugaring of let
  \end{itemize}
}

\end{document}