\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, \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}
This function has a major difference from the usual recursive
definitions you would give in other functional languages. We never
explicitly call \systemtinline{compose} in the inductive case. Instead
the \systemtinline{fold} keyword eagerly applies the body to all
inductive components in the argument. In this example, when we have a
\systemtinline{Branch}, the left and right subtrees are eagerly passed
to \systemtinline{compose}, so the body can only access the resulting
functions \systemtinline{f} and \systemtinline{g}.

\TODO{Why weird fold syntax}

As we can encode all \lang{} programs into System~T, \lang{} inherit
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 terminate and are well-founded does not
appear to greatly restrict what programs you can write in \lang{}. As
evidence of this, we have written the encoding algorithm from \lang{}
to System~T within \lang{}. 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.

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