@@ -4,43 +4,45 @@ Dependently typed programming languages, such as Agda \cite{norell2007thesis}
4and Coq \cite{Bertot2004}, have emerged in recent years as a promising approach
4and Coq \cite{Bertot2004}, have emerged in recent years as a promising approach
5to ensuring the correctness of software. The \Idris{} language
5to ensuring the correctness of software. The \Idris{} language
6\cite{Brady2011a} aims to take these ideas further, by providing support for
6\cite{Brady2011a} aims to take these ideas further, by providing support for
7−verification of general-purpose systems software. In contrast to Agda and Coq,
7+verification of general purpose systems software. In contrast to Agda and Coq,
8which have arisen from the theorem proving community, \Idris{} takes Haskell as
8which have arisen from the theorem proving community, \Idris{} takes Haskell as
9−its baseline. Recent Haskell extensions such as GADTs and type families have
9+its main influence. Recent Haskell extensions such as GADTs and type families have
10−given some of the power of dependent types to Haskell programmers. However,
10+given some of the power of dependent types to Haskell programmers. In the short
11+term this approach has a clear advantage, since it builds on a mature language
12+infrastructure with extensive library support.
13+Taking a longer term view, however,
11these extensions are inherently limited in that they are required to maintain
14these extensions are inherently limited in that they are required to maintain
12−backwards compatibility with existing Haskell programs. \Idris{}, being a new
15+backwards compatibility with existing Haskell implemtations. \Idris{}, being a new
13language, has no such limitation, essentially asking the question:
16language, has no such limitation, essentially asking the question:
15\begin{center}
18\begin{center}
16\emph{``What if Haskell had \emph{full} dependent types?''}
19\emph{``What if Haskell had \emph{full} dependent types?''}
17\end{center}
20\end{center}
19−It is important, for the sake of usability of a programming language, to provide
22+It is important for the sake of usability of a programming language to provide
20a notation which allows programmers to express high level concepts
23a notation which allows programmers to express high level concepts
21in a natural way. Taking Haskell as a starting point means that \Idris{} offers
24in a natural way. Taking Haskell as a starting point means that \Idris{} offers
22high level structures such as type classes, \texttt{do}-notation, primitive types
25high level structures such as type classes, \texttt{do}-notation, primitive types
23and monadic I/O, for example.
26and monadic I/O, for example.
24Nevertheless, it is important for the sake of correctness of the language implementation
27Nevertheless, it is important for the sake of correctness of the language implementation
25to have a small core language with well understood meta-theory
28to have a small core language with well understood meta-theory
26−\cite{Altenkirch2010}.
29+\cite{Altenkirch2010}.
28How can we achieve both of these goals?
30How can we achieve both of these goals?
30This paper describes a method for elaborating a high level dependently typed
32This paper describes a method for elaborating a high level dependently typed
31functional programming language to a low level core language based on dependent
33functional programming language to a low level core language based on dependent
32type theory. The method involves building an Embedded Domain Specific Language
34type theory. The method involves building an Embedded Domain Specific Language
33(EDSL) for constructing programs in the core language, using \emph{tactics}
35(EDSL) for constructing programs in the core language, using \emph{tactics}
34−directed by high level
36+directed by high level program syntax.
36−%This method allows higher level language constructs to be
37+As we shall see, this method allows higher level language constructs to be
37−%constructed in a straightforward manner.
38+constructed in a straightforward manner, without compromising the simplicity
39+of the underlying type theory.
39\subsection{Overview}
41\subsection{Overview}
41A dependently typed programming language relies on several components, many of
43A dependently typed programming language relies on several components, many of
42which are now well understood. For example, we rely on a type checker for
44which are now well understood. For example, we rely on a type checker for
43−the underlying type theory \cite{Chapman2005epigram,loh2010tutorial}, a
45+the core type theory \cite{Chapman2005epigram,loh2010tutorial}, a
44unification algorithm \cite{Miller1992} and an evaluator. However, it is less
46unification algorithm \cite{Miller1992} and an evaluator. However, it is less
45well understood how to combine these components effectively into a practical
47well understood how to combine these components effectively into a practical
46programming language. Therefore, the primary contribution of this paper is
48programming language. Therefore, the primary contribution of this paper is