@@ -422,13 +422,126 @@ $\vx$ requires.
422In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
422In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
423a tree of case expressions~\cite{Augustsson1985}.
423a tree of case expressions~\cite{Augustsson1985}.
425−\subsection{The Development Calculus \TTdev}
425+\subsection{From \Idris{} to \TT{}}
427−\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.
427+\TT{} is a very small language, consisting only of data declarations and pattern matching
428+function definitions. There is no significant innovation in the design of \TT{}, and this
429+is a deliberate choice --- it is a combination of small, well-understood components.
430+The kernel of the \TT{} implementation, consisting of a type checker, evaluator and
431+pattern match compiler, is less than 1000 lines of Haskell code. If we are confident
432+in the correctness of the kernel of \TT{}, and any higher level language feature
433+can be translated into \TT{}, we can be more confident of the correctness of the high
434+level language implementation that if it were implemented directly.
429−\subsection{The $\MO{Elab}$ meta-language}
436+The process of elaborating a high level language into a core type theory like \TT{} is,
437+however, less well understood, and presents several challenges depending on the
438+features of the high level language. Elaboration has been implemented in various different ways,
439+for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.
441+\subsubsection{Example Elaboration}
443+Consider the following \Idris{} function:
445+\begin{SaveVerbatim}{vadd}
447+vAdd : Num a => Vect a n -> Vect a n -> Vect a n
449+vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys
455+This adds corresponding elements of vectors of the same length. The vectors can contain
456+any numeric type, overloaded using the \texttt{Num} type class. In order to elaborate
457+this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.
459+The first step is to make the implicit arguments explicit, using a placeholder
460+to stand for the arguments we have not yet resolved. The type class argument is
461+also treated as an implicit argument, to which we give the name \texttt{c}:
463+\begin{SaveVerbatim}{vAddImp}
465+vAdd : (a : _) -> (n : _) -> Num a -> Vect a n -> Vect a n -> Vect a n
466+vAdd _ _ c (Nil _) (Nil _) = (Nil _)
467+vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
468+ = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
473+Next, we resolve the implicit arguments. Each implicit argument can only take
474+one value for this program to be type correct --- these are solved by a unification
477+\begin{SaveVerbatim}{vAddImpSolve}
479+vAdd : (a : Set) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n
480+vAdd a O c (Nil a) (Nil a) = Nil a
481+vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
482+ = (::) a k ((+) c x y) (vAdd a k c xs ys)
485+\useverb{vAddImpSolve}
487+Finally, to build the \TT{} definition, we need to find the type of each pattern variable
488+and state it explicitly. This leads to the \TT{} definition in Figure \ref{ttvadd},
489+switching to \TT{} notation from the ASCII \Idris{} syntax.
494+\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to
495+ \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\
498+\begin{array}{lccccccc}
500+\RW{var}\:\va\Hab\Set,\:\vc\Hab\TC{Num}\;\va\SC}\\
501+\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\
504+\va\Hab\Set,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\
505+\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;
506+\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk
510+\hg\FN{vAdd} & \va & (\suc\;\vk) & \vc
511+ & ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
512+ & ((\DC{::})\;\va\;\vk\;\vy\;\vys)
514+ & & \MRet{5}{((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))}
518+{Pairwise addition of vectors in \TT{}}
521+\subsubsection{An observation}
523+\Idris{} programs may contain several high level constructs not present in \TT{}, such
524+as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}
525+and \texttt{case} constructs. We would like the high level language to be as expressive
526+as possible, while remaining possible to translate to \TT{}.
528+Before considering how to achieve this, we make an observation about the distinction between
529+programming and theorem proving with dependent types, and appropriate mechanisms for
530+constructing programs and theorems:
432\begin{itemize}
532\begin{itemize}
433−\item $\MO{Check}\:\vt\:\cq\:(\vt, \vt)$
533+\item \remph{Pattern matching} is a convenient abstraction for humans to write programs,
534+in that it allows a programmer to express exactly the computational behaviour of a function.
535+\item \remph{Tactics}, such as those used in the Coq theorem prover~\cite{Bertot2004},
536+are a convenient abstraction for building proofs and programs by \remph{refinement}.
434\end{itemize}
537\end{itemize}
539+The idea behind the \Idris{} elaborator, therefore, is to use the high level program
540+to direct \demph{tactics} to build \TT{} programs by refinement. We implement the
541+elaborator as an Embedded Domain Specific Language (EDSL) in Haskell.
543+of this paper, we decribe the EDSL, and demonstrate how it can be used to implement
544+all of the high level features of \Idris{}.