blob: 0948073adea68709a282c4284290198052c4eee6 (
plain)
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
\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}
|
