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

\begin{document}
\section{Writing ARTyST Programs}%
\label{sec:reducer}

We have used \lang{} to write two non-trivial programs that can be
embedded in System~T. The first is a fuelled reducer for
System~T. Given \(n\) units of fuel, the reducer will perform \(n\)
steps of complete~development~\cite{cd} on a System~T term. The second
program is the encoding from \lang{} to System~T. This takes a
type-annotated \lang{} program and encodes it as a System~T term.

\TODO{describe the syntactic sugar I have added}

\subsection{Fuelled System~T Reducer}%
\label{subsec:reducer}

Given enough fuel to work with, a fuelled reducer takes a term as
input and reduces it to normal form. Our fuelled reducer operates
using term rewriting. For each unit of fuel, we perform one step of
complete development; we reduce \emph{all} beta redices in the input
term simultaneously. As System~T is confluent and strongly
normalising, complete development will converge on the normal form of
the input term.

We define System~T terms as the inductive type in
\cref{lst:term-ty}. The compiler, detailed in \cref{M-sec:compiler}
makes a few small changes to the syntax to be more descriptive. Most
notably, products are indexed by labels instead of by position. For
example, the \verb|Primrec| constructor takes a product with three
components: the target, and the branches for zero and successor. As
\lang{} is simply typed, there is no way to enforce terms are
correctly typed nor correctly scoped.

\begin{listing}
  \begin{verbatim}
data Term
  [ Var: Nat
  ; Zero: <>
  ; Suc: Term
  ; Primrec: <Zero: Term; Suc: Term, Target: Term>
  ; Abs: Term
  ; App: <Fun: Term, Arg: Term>
  ]
  \end{verbatim}
  \caption{Inductive type representing System~T terms.}\label{lst:term-ty}
\end{listing}

An example function is \verb|rename|, taking a term and a renaming
function \verb|Nat -> Nat|, and updating all variables according to
the renaming function. The program is in \cref{lst:rename}. We use
\verb|~| as the syntax for \roll{} and \verb|foldcase| is syntactic
sugar for performing a \foldkw{} whose body immediately pattern
matches on the induction hypothesis. Recall that a fold fills the
shape type with the motive. For example, for the \verb|App| branch,
\verb|p| has type
\verb|<Fun: (Nat -> Nat) -> Term; Arg: (Nat -> Nat) -> Term>|. As
application doesn't bind any variables, we can pass the renaming
\verb|f| to the inductive components without modification. For
abstraction and primitive recursion, we have to lift the renaming
function, corresponding to binding a variable.

\begin{listing}
  \begin{verbatim}
let rename (t : Term) : (Nat -> Nat) -> Term =
  foldcase t by
    { Var n     => \f => ~(Var (f n))
    ; Zero _    => \f => ~(Zero <>)
    ; Suc r     => \f => ~(Suc (r f))
    ; Primrec p => \f =>
      ~(Primrec <Zero: p.Zero f; Suc: p.Suc (lift f); Target: p.Target f>)
    ; Abs r     => \f => ~(Abs (r (lift f)))
    ; App p     => \f => ~(App <Fun: p.Fun f; Arg: p.Arg f>)
    }
  \end{verbatim}
  \caption{Implementation of term renaming.}\label{lst:rename}
\end{listing}

The main driver in the reducer is the \verb|step| function, which
performs a complete development of a term. We give its definition in
\cref{lst:step}. By induction, all terms within the \verb|foldcase|
have been completely developed. Most cases pass through their
arguments unchanged: the only reductions for \(\suc~t\) happen within
\(t\) for instance. The two interesting cases are \verb|Primrec| and
\verb|App|. Here we match on the ``active'' term, performing a
reduction if possible. If the active term is either a neutral
(\verb|Var|) or absurd (\verb|Zero| as a function) we return the
inductive argument without further computation applied. Our fuelled
reducer applies the \verb|step| function to the input for each unit of
fuel it is given.

\begin{listing}
  \begin{verbatim}
let step (t : Term) : Term =
  foldcase t by
    { Var n     => ~(Var n)
    ; Zero _    => ~(Zero <>)
    ; Suc t     => ~(Suc t)
    ; Primrec p =>
      let default = ~(Primrec p) in
      case p.Target of
        { Var _     => default
        ; Zero _    => p.Zero
        ; Suc t     =>
          sub p.Suc [ ~(Primrec <Zero: p.Zero; Suc: p.Suc; Target: t>) ]
        ; Primrec _ => default
        ; Abs _     => default
        ; App _     => default
        }
    ; Abs t     => ~(Abs t)
    ; App p     =>
      let default = ~(App p) in
      case p.Fun of
        { Var _     => default
        ; Zero _    => default
        ; Suc t     => default
        ; Primrec _ => default
        ; Abs t     => sub t [ p.Arg ]
        ; App _     => default
        }
    }
  \end{verbatim}
  \caption{Implementation of complete development.}\label{lst:rename}
\end{listing}

\TODO{explain why fuel is necessary for the reducer}

\subsection{Encoding Algorithm}%
\label{subsec:encoding}

In \cref{M-sec:encoding} we described a process to embed \lang{}
within System~T. We have written this algorithm in \lang{} itself,
simultaneously mechanising the conversion and proving it is
terminating. Our input is type-annotated \lang{} terms, and we output
unannotated System~T terms as in \cref{lst:term-ty}. Each phase is
accompanied by its own inductive types representing types and
type-annotated terms.

Folds in \lang{} are destructive---the inductive components used to
generate the induction hypothesis are unnamed. This has some
interesting interactions with encoding the \(\mathsf{distrib}\) term
in phase one, and implementing the \mapkw{} pseudo-operator in phase
two. Both of these functions are defined by induction on types with
motives that are functions returning terms. This means that the
inductive hypothesis for each branch consists of a type constructor
filled with some number functions. To construct a term, we need not
only the subterms provided by the induction hypothesis, but we also
need the types of those subterms. To preserve this typing information,
both \(\mathsf{distrib}\) and \mapkw{} must return a pair of type and
term.

\begin{listing}
  \begin{verbatim}
; Arrow p =>
  let myTy = ~(Arrow <Dom: p.Dom.Ty []; Cod: p.Cod.Ty []>) in
  < Ty:   \env => myTy
  ; Term: \env, k, s => ~(Abs ~(Abs ~(Tup
    [ <Ty: s;    Term: ~(Var 0)>
    ; <Ty: myTy; Term: ~(Var 1)>])))
  >
  \end{verbatim}
  \caption{The branch of \(\mathsf{distrib}\) corresponding to
    function types.}\label{lst:distrib-arrow}
\end{listing}

As a concrete example, consider the branch of \(\mathsf{distrib}\)
over a function type, shown in \cref{lst:distrib-arrow}. The induction
hypothesis is a pair of motives generated from the domain and
codomain. The motive is a pair of functions. The \verb|Ty| component
takes an environment and returns a compiled type. The \verb|Term|
component takes an environment, a chosen type variable \verb|k| and a
type \verb|S| and returns a term distributing an accumulator for
\verb|S| at index \verb|k| outside of the type constructor. Ideally,
we would only need the \verb|Term| component of the pair. However, the
type annotations needed for the tuple force us to also compute the types.

From a language design standpoint, we could have chosen that \foldkw{}
is non-destructive. The inductive hypothesis would have the form
\(\sub{A}{X/(\mu X. A) \times B}\) for shape \(A\) and motive \(B\). This is
exactly as expressive as the chosen type, with inductive hypothesis
\(\sub{A}{X/B}\). We chose to use the simpler motive inductive
hypothesis for two reasons: it has a simpler categorical semantics;
many folds do not need the non-destructive argument.

\subsection{Composing the Two Programs}

Our encoding algorithm introduces many administrative
\(\beta\)-redexes. We manually reduced many of them in the examples at the
end of each phase in \cref{M-sec:encoding}. The final desugaring in
phase seven also introduced many redexes when eliminating \letkw{}
expressions. Thus the ``efficiency'' of an encoded program can be
improved by performing the simple partial evaluation of our fuelled
reducer.

Even with a partial reduction pass, our encoder can still have some
performance issues. Neither \lang{} nor System~T have \emph{commuting
conversions}; equations about how two case splits, folds or primitive
recursions interact. This means two contextually equivalent terms are
not equal in the equational theory. An example of this are the
\systemtinline{compose} and \systemtinline{compose'} functions from
encoding phase two. Because it performs fewer pattern matches,
\systemtinline{compose'} would have a encoding than
\systemtinline{compose} despite containing the same information.

There are no equations we can add to resolve this for \foldkw{} or
\primreckw{}. \TODO{how do I mitigate this?}

\end{document}