git.iko.soy/Idris-dev
on 64b7cfd help sign in
Idris-dev/impl-paper/overview.tex
33 lines 1.5 kB history raw
1\section{overview}
3High level view of steps we've taken to implement this new version:
5\begin{itemize}
6\item Syntax tree for raw and well-typed terms
7\item An evaluator for well-typed terms
8\item The important bit: a simple type checker. No unification or
9 inference.
10\begin{itemize}
11 \item It is extremely tempting to add implicit arguments and unification to the
12 type checker. This is what I did in the first Idris prototype: I learned
13 that it was a bad idea! Scope is a big problem.
14\end{itemize}
15\item The proof state and a tactic engine (Oleg style~\cite{mcbride-thesis}).
16\begin{itemize}
17 \item Dealing with names: typechecking and evaluation in a context, managing de Bruijn
18 indices becomes tricky. Instead: global names, local names during construction,
19 and de Bruijn indices when done.
20\end{itemize}
21\item Unification, and incorporation into the tactic engine.
22\begin{itemize}
23 \item Note that this can introduce constraints on hole ordering. If we can't satisfy them,
24 report an error.
25\end{itemize}
26\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and
27 constructing derived tactics.
28\end{itemize}
30For the high level language: we need nothing more than the core type theory,
31and a way of putting stuff together. So we typecheck each pattern match clause
32individually, in an appropriate context. There is no need for the core type
33theory to have pattern matching.