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

\begin{document}
\section{Encoding Artyst}%
\label{sec:encoding}

We have devised an encoding of \lang{} into System~T. The encoding has
seven phases. 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
and C-style unions, which we will later need to remove. The full list
of seven phases are:
\begin{enumerate}
\item changing the \roll{} operator so that all inductive components
  are collected together in a list.
\item encoding inductive types using a list-indexed heap.
\item encoding lists using eliminators.
\item introducing unions to encode sums as a tagged union.
\item encoding products as an indexed union.
\item encoding unions of System~T types.
\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 \TODO{type syntax: \(\mu X. (\nat \to \nat) + X \times X\)},
where leaves are labelled by unary functions on naturals. In our first
example we construct a balanced binary tree of depth \(n + 1\),
filling leaves with a given function \systemtinline{f}. This will
demonstrate how we encode constructors for inductive types.
\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}

We will also use the \systemtinline{compose} function given in the
introduction. This will show how we encode destructors for inductive
types.

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

Recall the typing judgement for \roll{} in \cref{M-fig:lang-ty}. The
argument has type \(\sub{A}{X/\mu X. A}\). Using substitution means that
inductive components can appear scattered throughout a vessel of this
type. Take the inductive type \(\mu X. \lgroup (1 + \nat \times X + \mu Y. (1 +
X \times Y)) \times (1 + X) \rgroup\) as an example. The inductive parameter
\(X\) appears in three seperate locations, including within another
inductive type. A vessel of this shape could have any number of
inductive components.

Collecting all the inductive components 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 typing judgement.
\[
\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 including the inductive components within the argument of
\roll{}, we instead collect them into an external list. We fill the
vessel \(u\) with pointers to the values within \(t\). 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}
\]

To transform an argument for \roll{} \(x\) into the arguments for
\roll*{}, we take the projections of the term
\[
  \mathsf{distrib}^{\nat}_{\Lambda X. A}~(
    \maptm{X}{A}~(
      \lambda y, acc. \tuple{\mathsf{snoc}~acc~y, \mathsf{length}~acc}
    )~x
  )~\mathsf{nil}
\]
The \mapkw{} replaces each inductive component \(\mu X. A\) with an
accumulator \(\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times
\nat\), which extends a list with the component and records the
component's index in the list. We then ``distribute'' the accumulator
over the vessel using the \(\mathsf{distrib}\) meta-operator. We finally
give the empty list as the initial accumulator.

Given a
well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X
\in \Psi\), a type environment \(\alpha\) and a type \(S\),
\(\mathsf{distrib}^{\alpha, S}_{\Lambda X. A}\) has type
\[
\suball{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \suball{A}{\alpha}.
\]
\(\mathsf{distrib}\) calls each accumulator of type in the vessel in
sequence. We give the details in \cref{M-sec:distrib}.

We require a few operations on lists to compute this transformation:
\begin{description}
  \item[\(\mathsf{nil}\)] the empty list;
  \item[\(\mathsf{cons}\)] adds an element to the head of a list;
  \item[\(\mathsf{snoc}\)] adds an element to the tail of a list;
  \item[\(\mathsf{length}\)] computes the number of elements in a
    list; and
  \item[\(\mathsf{index}\)] retrieves a value from a list by position.
\end{description}

We give the equations these operators satisfy below.
\begin{align*}
\mathsf{snoc}~\mathsf{nil}~v &= \mathsf{cons}~v~\mathsf{nil} &
\mathsf{snoc}~(\mathsf{cons}~t~u)~v &= \mathsf{cons}~t~(\mathsf{snoc}~u~v) \\
\mathsf{length}~\mathsf{nil} &= \zero &
\mathsf{length}~(\mathsf{cons}~t~u) &= \suc~(\mathsf{length}~u) \\
\mathsf{index}~(\mathsf{cons}~t~u)~\zero &= t &
\mathsf{index}~(\mathsf{cons}~t~u)~(\suc~n) &= \mathsf{index}~u~n
\end{align*}

At the end of this phase, the \systemtinline{compose} example is
unchanged. The \systemtinline{balanced} example reduces to the below
code. A \systemtinline{Leaf} has no inductive components, so the list
passed to \roll*{} in the \zero{} branch is empty. The \suc{} branch
uses the same variable \systemtinline{tree} in two different positions
in the list. To keep our future examples small, we will instead use
the list \systemtinline{[tree]} with indices \systemtinline{(0, 0)}.
\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 use naturals as
pointers. The idea is that the heap index describes the path taken
through the term to reach a particular entry, whilst the pointers
describe the next step along the path.

We chose to use a heap encoding over another encoding strategy by
elimination of the other strategies. 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:encoding-strategies} 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 its tail is the path
within this component. Instead of eagerly fix pointers as described
earlier, we compute new paths lazily during a fold. This simplifies
the \roll*{} operation as we do not need to fixup the entire heap.

\begin{figure}
  \begin{align*}
    \roll*~ts~x &\coloneq \tuple*{
      \suc~(\mathsf{max}~(\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})\). We present the encoding of
\roll*{} and \foldkw{} in \cref{fig:phase-2-encode}. We add two new
operators for working with lists:
\begin{description}
  \item[\(\mathsf{max}\)] for calculating the maximum from a list,
    given a function converting values to naturals; and
  \item[\(\mathsf{match}\)] for pattern matching on a list as either
    \(\mathsf{nil}\) or \(\mathsf{cons}\)
\end{description}
These operators satisfy the following equations:
\begin{align*}
  \mathsf{max}~f~\mathsf{nil} &= 0 &
  \domatch{\mathsf{nil}}{\mathsf{nil}. f; \mathsf{cons}~x~y. g} &= f \\
  \mathsf{max}~f~(\mathsf{cons}~t~u) &= f~t \sqcup u &
  \domatch{\mathsf{cons}~t~u}{\mathsf{nil}. f; \mathsf{cons}~x~y. g}
    &= \sub{g}{x/t, y/u}
\end{align*}

Computing the maximum value from a list is necessary to correctly
determine the recursive depth to use when folding over a value. It is
also the primary reason why infinite inductive types are
forbidden. Recall the inductive type \(\mu X. 1 + (\nat \to X)\) of
countable trees. To compute the recursive depth of such a tree, we
need to compute the maximum of an arbitrary countable sequence. Thus
we cannot encode such infinite types.

We also add \(\mathsf{match}\) on lists. We need this to determine
whether a path is addressing the root entry or one of its inductive
components.

We now return to our examples. After simplifying using the equational
theory we recover
the below value for \systemtinline{balanced}. In each branch we
increase the recursive depth by one and create a new heap.
\begin{listing}[H]
\begin{systemt}
let balanced n f = primrec n with
  Zero => (Suc Zero, fun xs =>
    match xs with
      []      => Leaf f
    | x :: xs => snd (index [] x) xs)
| Suc (depth, heap) =>
    (Suc depth, fun xs =>
      match xs with
        []      => Branch (0, 0)
      | x :: xs => snd (index [(depth, heap)] x) xs)
\end{systemt}
\vspace{-\baselineskip}
\end{listing}
And below is the updated value of \systemtinline{compose}. In the
\systemtinline{Suc} branch, the \systemtinline{update} function
recursively looks up a pointer in the result map. The value
\systemtinline{x} is the result of mapping \systemtinline{update}
through the payload at \systemtinline{index}.
\begin{listing}[H]
\begin{systemt}
let compose (depth, heap) =
  let go = primrec depth with
    Zero   => arb
  | Suc ih => fun index =>
    let update = fun i => ih (snoc index i) in
    let x = match heap index with
      Leaf i        => Leaf (update i)
    | Branch (i, j) => Branch (update i, update j)
    in match x with
      Leaf f        => f
    | Branch (f, g) => fun x => f (g x)
  in go []
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

Again to keep our example small, we will perform a commuting
conversion within the \systemtinline{Suc} branch to combine the two
match statements into one. After some further beta reductions, we
obtain the simplified definition

\begin{listing}[H]
\begin{systemt}
let compose (depth, heap) =
  let go = primrec depth with
    Zero   => arb
  | Suc ih => fun index =>
    let update = fun i => ih (snoc index i) in
    match heap index with
      Leaf i        => update i
    | Branch (i, j) => fun x => update i (update j 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.

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~\cite{if+equals}.

The encoding of \(\mathsf{snoc}~t~u\), adding element \(u\) to the
tail of the list \(t\), is similar:
\[
\tuple{
  \suc~t.0,
  \lambda x.\mathsf{if}~x = t.0~\mathsf{then}~u~\mathsf{else}~t.1~x
}
\]
The new list is again 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 \(\mathsf{max}~f~t\) by primitive recursion on the length of
the list \(t\).
\[\doprimrec{t.0}{\zero}{x}{f~x.0 \sqcup x.1}\]

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.

Our eliminator encoding could also include \(\mathsf{max}\). We avoid
this for two reasons. Firstly, we can compute the maximum using the
length and indexing functions, so adding an explicit eliminator is
redundant information. Secondly, most lists do not need to know their
maximum. We only need the maximum of lists passed to \roll*{}. Most
lists we create are indices for \foldkw{}, where there is no reason to
compute the maximum. Even when we do need to compute the maximum, most
lists passed to \roll*{} have a static length making the
\(\mathsf{max}\) operator easy to partially evaluate.

After phase three, our example for \systemtinline{balanced} beta
reduces to the below. This example demonstrates both pattern matching
and indexing lists. In the \systemtinline{Suc} branch, the variable
\systemtinline{dh} stores the result of indexing the single list
\systemtinline{[(depth, heap)]}.
\begin{listing}[H]
\begin{systemt}
let balanced n f = primrec n with
  Zero => (Suc Zero , fun (length, idxs) =>
    if length == 0 then Leaf f else
      snd arb (length - 1, fun i => idxs (Suc i)))
| Suc (depth, heap) => (Suc depth, fun (length, idxs) =>
    if length == 0 then Branch (0, 0) else
      let dh = if idxs 0 == 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 the following. Most of the
changes happened to the \systemtinline{update} function as it computes
the \(\mathsf{snoc}\) on a given index.
\begin{listing}[H]
\begin{systemt}
let compose (depth, heap) =
  let go = primrec depth with
    Zero   => arb
  | Suc ih => fun (length, idxs) =>
    let update =
      fun i => ih (Suc length, fun j =>
        if j == length then i else idxs j)
    match heap (length, idxs) with
      Leaf i        => update i
    | Branch (i, j) => fun x => update i (update j x)
  in go (Zero, arb)
\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_{\ell \in I} A_\ell\) by the pair \(\nat \times \bigsqcup_{\ell \in I} A_\ell\)
of a tag indicating the variant, and a union which can contain a value
from any variant.

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

We encode the injection into a sum \(\ell~t\) by the pair \(\tuple{\ell,
  \mathsf{inj}~\ell~t}\). We encode pattern matching
\((\casetm{t}{\ell~x_\ell}{t_\ell}{\ell})\) by the term \(
(\casetm{t.0}{\ell}{\sub{t_\ell}{x_\ell/\mathsf{prj}~t.1~\ell}}{\ell}) \) 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.

Our two examples reduce even further. We obtain the following for
\systemtinline{balanced} after encoding \systemtinline{Leaf} and
\systemtinline{Branch} as tagged unions.

\begin{listing}[H]
\begin{systemt}
let balanced n f = primrec n with
  Zero => (Suc Zero, fun (length, idxs) =>
    if length == 0 then (Leaf , inj Leaf f) else
      snd arb (length - 1, fun i => idxs (Suc i)))
| Suc (depth, heap) => (Suc depth, fun (length, idxs) =>
    if length == 0 then (Branch, inj Branch (0, 0)) else
      let dh = if idxs 0 == 0 then (depth, heap) else arb in
      snd dh (length - 1, fun i => idxs (Suc i)))
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

The \systemtinline{compose} example demonstrates how pattern matching
is encoded. We first pattern match on the tag and then project the
payload into the corresponding type.

\begin{listing}[H]
\begin{systemt}
let compose (depth, heap) =
  let go = primrec depth with
    Zero   => arb
  | Suc ih => fun (length, idxs) =>
    let update =
      fun i => ih (Suc length, fun j =>
        if j == length then i else idxs j)
    let (tag, v) = heap (length, idxs) in
    match tag with
      Leaf   => update (prj v Leaf)
    | Branch =>
        let (i, j) = prj v Branch in
        fun x => update i (update j x)
  in go (Zero, arb)
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

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

We will continue following the work of \textcite{oleg} to encode away
products. A product \(\prod_i A_i\) is encoded as a function \(\nat \to
\bigsqcup_i A_i\) from indices to values. This is similar to the
encoding for lists, with only a couple of small variations. First, we
statically know the length of a product, so we do not need to include
it within its type. Secondly, a product can store values from
different types whilst a list is homogenous, so we need to use the
union to make it homogenous.

We encode tupling \(\tuple{\rangeover{t_i}{i}}\) as the case split \(\lambda
x. \casetm{x}{i}{\mathsf{inj}~i~t_i}{i}\). The projection \(t.i\) is
encoded as the application \(\mathsf{prj}~(t~i)~i\).

At this phase the encodings of our example functions,
\systemtinline{balanced} and \systemtinline{compose'}, become too
cluttered to be useful. Instead we will consider the
\systemtinline{dupfirst} function, of type \((\nat \to \nat) \times \nat \to
(\nat \to \nat) \times (\nat \to \nat) \times \nat\), which takes a pair of a
function and value, and duplicates the first component of the pair.
Originally defined as \systemtinline{let dupfirst t = (t.0, t.0, t.1)},
after encoding products the function becomes
\begin{listing}[H]
\begin{systemt}
let dupfirst t = fun x => match x with
  0 => inj 0 (prj (t 0) 0)
| 1 => inj 1 (prj (t 0) 0)
| 2 => inj 2 (prj (t 1) 1)
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

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

At this point, the only type former we use that is not present in
System~T is the union type.\@ \textcite{oleg} gives an inductive
encoding for binary unions. We instead use an encoding for unions
derived from the argument form of types. Given we have a family of
types \(A_i\) in argument form, their union \(\bigsqcup_i A_i\) is the
concatenation \(A_1 \append A_2 \append \cdots \append A_n\). To inject
type \(A_k\) into the union, we ignore the function arguments for all
the other types. To project type \(A_k\) out of the union, we pass
\(\mathsf{arb}\) to all the other arguments.

Using this argument-form union, we remove the need to perform
induction on types, and only have to iterate over the number of types
in the union. This also simplifies the proof that our encoding of the
union satisfies the required beta reduction rule. In exchange, our
union encoding is neither idempotent nor commutative, and generally
results in larger types than \posscite{oleg} encoding.

The \systemtinline{dupfirst} example reduces to the below. If we
instead used \posscite{oleg} encoding then the returned function would
take only a single argument \systemtinline{x}.
\begin{listing}[H]
\begin{systemt}
let dupfirst t = fun x => match x with
  0 => fun x y => t 0 x
| 1 => fun x y => t 0 y
| 2 => fun x y => t 1 arb
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

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

This final phase of encoding performs desugaring; there are only a
couple of remaining operations to encode. These include case splitting
on a natural number; constructing an arbitrary value of a type; and
\letkw{} expressions.

We encode case splitting on a number by a chain of equality tests. If
all the tests fail, we will return an arbitrary value. We can
construct an arbitrary value at any type by using the function that
constantly returns zero. Let expressions are given their usual
functional decoding as an abstraction applied immediately to an
argument.

The \systemtinline{dupfirst} example desugars into the following
expression:
\begin{listing}[H]
\begin{systemt}
let dupfirst t = fun x =>
  if x == 0 then fun x y => t 0 x else
  if x == 1 then fun x y => t 0 y else
  if x == 2 then fun x y => t 1 0 else
    fun x y => 0
\end{systemt}
\vspace{-\baselineskip}
\end{listing}

\end{document}