sec/compiler.ltx


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

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

\begin{document}
\section{Idris 2 Compiler}%
\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}