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

\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}.
We use the keyword \verb|data| to introduce a fixed point type. Sums
are given in square brackets and products in angle brackets.  As
\lang{} is simply typed, there is no way to statically enforce terms
are correctly typed nor correctly scoped, but one can write scope and
type checkers within \lang{}.

\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 induction hypothesis
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:step}
\end{listing}

Our reducer only applies \(\beta\)-reduction. It is also possible to
perform \(\eta\)-contraction as computing a strengthened term requires only
structural induction.

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

In \cref{M-sec:encoding} we described an algorithm to embed \lang{}
within System~T. We have written this algorithm in \lang{} itself,
simultaneously mechanising the conversion and indirectly proving it is
terminating. Our input is a type-annotated \lang{} term, and we output
an unannotated System~T term as in \cref{lst:term-ty}. Each phase is
accompanied by its own inductive types representing the phases' types
and terms. To compute the encoding, any term formers that are not in
System~T must be annotated with their types. For simplicity, our
finite sums and products are over unlabelled lists of types instead of
finite sets.

Folds in \lang{} are destructive---the inductive components used to
generate the induction hypothesis are inaccessible. 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 of the form \(\text{Type} \to \text{Env} \to
\text{Term}\). Our term representations require type annotations but
any subtypes are inaccessible. So, we program \(\mathsf{distrib}\) and
\(\mathsf{map}\) to return a pair of term and type.

\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 motive
type is
\verb|<Ty : List Type -> Type; Term: List Type -> Nat -> Type>|. The
\verb|Ty| component is the result of type substitution and the
\verb|Term| component is the result of \(\mathsf{distrib}\).  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 as 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 introduces many redexes when eliminating \letkw{}
expressions. Thus the ``efficiency'' of an encoded program can be
improved by partially evaluating 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 is our
simplification of the \systemtinline{compose} function from encoding
phase two. Because it performs fewer pattern matches, the second
\systemtinline{compose} would have a ``simpler'' encoding than the
original despite containing the same information.

\TODO{System~T self reducer}

\end{document}