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

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

\TODO{
  \begin{itemize}
    \item describe that I have a type checker and compiler implemented in Idris
    \item explain what intentionally well-scoped syntax is
    \item justify why I used intentionally well-scoped syntax
    \item describe how type checking produces a derivation
    \item explain the derivation is runtime erased
    \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}
}

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