Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

36 lines (32 sloc) 1.662 kb
\subsection{Overview}
High level view of steps we've taken to implement this new version:
\begin{itemize}
\item Syntax tree for raw and well-typed terms
\item An evaluator for well-typed terms
\item The important bit: a simple type checker. No unification or
inference.
\begin{itemize}
\item It is extremely tempting to add implicit arguments and unification to the
type checker. This is what I did in the first Idris prototype: I learned
that it was a bad idea! Scope is a big problem.
\end{itemize}
\item The proof state and a tactic engine (Oleg style~\cite{McBride1999}).
\begin{itemize}
\item Dealing with names: typechecking and evaluation in a context, managing de Bruijn
indices becomes tricky. Instead: global names, local names during construction,
and de Bruijn indices when done.
\end{itemize}
\item Unification, and incorporation into the tactic engine.
\begin{itemize}
\item Note that this can introduce constraints on hole ordering. If we can't satisfy them,
report an error.
\end{itemize}
\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and
constructing derived tactics, from a high level syntax withe implicit arguments.
\item Adding primitive operators and a link to Epic~\cite{brady2011epic}.
\item Advanced elaborations: using declarations, where clauses, type classes.
\end{itemize}
For the high level language: we need nothing more than the core type theory,
and a way of putting stuff together. So we typecheck each pattern match clause
individually, in an appropriate context. There is no need for the core type
theory to have pattern matching.
Jump to Line
Something went wrong with that request. Please try again.