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

\begin{document}
\section{Idris 2 Compiler for Artyst}%
\label{sec:compiler}

To aid the development of the System~T reducer and encoding
algorithms, we have implemented a type checker and compiler for
\lang{}. The compiler is written in Idris~2~\cite{idris}, a
dependently typed programming language. The compiler is split into
three main components:
\begin{itemize}
  \item First we have a parser based on \textcite{alg-parsing}. The
    parser interface guarantees that we process the input without
    backtracking. This produces an intrinsically-well-scoped abstract
    syntax tree.

  \item Second we perform type checking using a bidirectional
    algorithm~\cite{bidir}. Along with the usual type checking result,
    the algorithm produces a runtime-erased typing derivation.

  \item Finally we compile the term to Guile~Scheme~\cite{guile}. By
    requiring an erased type derivation, the compiler can statically
    guarantee it will only ever have to process well-typed terms.
\end{itemize}

\subsection{Parser}
\TODO{
  \begin{itemize}
    \item summarise \textcite{bidir}
    \item explain dependent state
    \item explain what intentionally well-scoped syntax is
    \item justify why I used intentionally well-scoped syntax
  \end{itemize}
}

\subsection{Bidirectional Type Checker}
\TODO{
  \begin{itemize}
    \item describe how type checking produces a derivation
    \item explain the derivation is runtime erased
    \item justify extrinsic derivation
    \item justify the derivation having no runtime cost
    \item describe why knowing there is a derivation is necessary
    \item explain why these extra features do not guarantee compiler correctness
  \end{itemize}
}

\subsection{Scheme Backend}
\TODO{
  \begin{itemize}
    \item justify how dynamic types make Scheme a good compilation target
    \item describe how products are compiled to assoc-lists
    \item describe how sums are compiled to tagged values
    \item describe how dynamic typing removes the need for roll
    \item explain why fold needs to know the term has a valid type
    \item explain why fold must be compiled recursively with map
  \end{itemize}
}

\end{document}