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

\begin{document}
\section{Introduction}%
\label{sec:intro}

System~T is a simply-typed lambda calculus (STLC) with natural numbers
and primitive recursors. It is arguably the simplest system for
higher-order computation~\cite{stlc-simple}. In this paper we explore
the expressive power of System~T by designing a new language that
encodes into System~T.

Our language, \lang{}, adds the regular types~\cite{regular} to
System~T. These include sums, products and some inductive
types. Whilst there are well-known techniques to encode most of these
types in System~T~\cites{oleg}{longley-normann}, \lang{} is the first
known language to do so automatically. Below is a small pseudocode
snippet of \lang{}. The function takes a binary tree of unary
functions and outputs their right-to-left composition.
\begin{listing}[H]
  \begin{systemt}
let compose (tree : Tree) = foldmatch tree with
  Leaf f         => f
| Branch (f , g) => fun x => f (g x)
  \end{systemt}
  \vspace{-\baselineskip}
\end{listing}

Note that we never explicitly call \systemtinline{compose} with a
subtree. Instead the \foldkw{} eagerly recurses on all subtrees
automatically. In this example, when our tree is a
\systemtinline{Branch}, the fold composes each subtree into functions
\systemtinline{f} and \systemtinline{g} respectively.

Our \foldkw{} syntax is more similar to eliminators~\cite{eliminators}
than the explicit recursion in other functional languages. We use this
eliminator style to ensure all recursion is structural. If we used
explicit recursion, we would need complex checks for structural
recursion, like in Agda~\cite{agda} and Idris~2~\cite{idris}.

As we can encode all \lang{} programs into System~T, \lang{} inherits
some of System~T's metatheory for free. In particular, as System~T is
strongly normalising~\cite{syst-sn}, all \lang{} programs must
terminate. Requiring programs to terminate and use structural
recursion does not appear to greatly restrict what programs you can
write in \lang{}. As evidence, we have written the encoding algorithm
from \lang{} to System~T within \lang{} itself. We have also produced
a fuelled System~T reducer; given enough fuel, it strongly normalises
any well-typed System~T term.

Developing these non-trivial recursive programs requires good tools
for using \lang{}. To that end, we have implemented a certifying type
checker and a compiler into Scheme. Our type checker not only checks
whether a \lang{} program is well/ill-typed, but it also provides a
proof for its decision. The compiler needs this certificate when
compiling \lang{} into Scheme, so that it has enough type information
to compile \foldkw{}.

\subsubsection*{Contributions}%
In this paper we:
\begin{itemize}[nosep]
  \item contrast different methods for encoding inductive types in
    System~T (\cref{M-subsec:encoding-strategies});
  \item give the syntax, typing rules and equational theory for
    \lang{} (\cref{M-sec:lang});
  \item explain how to encode \lang{} into System~T by giving a
    seven-phase encoding algorithm (\cref{M-sec:encoding});
  \item demonstrate usability of \lang{} over System~T by writing a
    fuelled System~T reducer (\cref{M-subsec:reducer});
  \item demonstrate expressiveness of \lang{} by writing the encoding
    algorithm within \lang{} (\cref{M-subsec:encoding}); and
  \item describe a certifying type checker and a compiler for \lang{}
    implemented in Idris~2 (\cref{M-sec:compiler}).
\end{itemize}

\end{document}