git.iko.soy/Idris-dev
on b8a2bbf help sign in
Idris-dev/impl-paper/overview.tex
35 lines 1.6 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, from a high level syntax withe implicit arguments.
28\item Advanced elaborations: using declarations, where clauses.
29\item Adding primitive operators and a link to Epic~\cite{epic-tfp}.
30\end{itemize}
32For the high level language: we need nothing more than the core type theory,
33and a way of putting stuff together. So we typecheck each pattern match clause
34individually, in an appropriate context. There is no need for the core type
35theory to have pattern matching.