3Dependently typed programming languages, such as Agda \cite{norell2007thesis}
4and Coq \cite{Bertot2004}, have emerged in recent years as a promising approach
5to ensuring the correctness of software. Type checking ensures a program has
6the intended meaning; \emph{dependent} types, where types may be predicated
7on values, allow a programmer to give a program a \emph{precise} type and
8hence have increased confidence of its correctness.
10\cite{Brady2011a} aims to take this ideas further, by providing support for
11verification of \emph{general purpose} systems software. In contrast to Agda and Coq,
12which have arisen from the theorem proving community, \Idris{} takes Haskell as
13its main influence. Recent Haskell extensions such as GADTs and type families have
14given some of the power of dependent types to Haskell programmers. In the short
15term this approach has a clear advantage, since it builds on a mature language
16infrastructure with extensive library support.
17Taking a longer term view, however,
18these extensions are inherently limited in that they are required to maintain
19backwards compatibility with existing Haskell implementations. \Idris{}, being a new
20language, has no such limitation, essentially asking the question:
23\emph{``What if Haskell had \emph{full} dependent types?''}
26By \emph{full} dependent types, we mean that there is no restriction on which
27values may appear in types. It is important for the sake of usability of a
28programming language to provide a notation which allows programmers to express
29high level concepts in a natural way. Taking Haskell as a starting point means
30that \Idris{} offers a variety of high level structures such as type classes,
31\texttt{do}-notation, primitive types and monadic I/O, for example.
32Furthermore, a goal of \Idris{} is to support high level domain specific
33language implementation, providing appropriate notation for \emph{domain
34experts} and \emph{systems programmers}, who should not be required to be type
35theorists in order to solve programming problems. Nevertheless, it is
36important for the sake of correctness of the language implementation to have a
37well-defined core language with well-understood meta-theory \cite{Altenkirch2010}.
38How can we achieve both of these goals?
40This paper describes a method for elaborating a high level dependently typed
41functional programming language to a low level core language based on dependent
42type theory. The method involves building an Embedded Domain Specific Language
43(EDSL) for constructing programs in the core language, using \emph{tactics}
44directed by high level program syntax.
45As we shall see, this method allows higher level language constructs to be
46constructed in a straightforward manner, without compromising the simplicity
47of the underlying type theory.
49\subsection{Contributions}
51A dependently typed programming language relies on several components, many of
52which are now well understood. For example, we rely on a type checker for
53the core type theory \cite{Chapman2005epigram,loh2010tutorial}, a
54unification algorithm \cite{Miller1992} and an evaluator. However, it is less
55well understood how to combine these components effectively into a practical
58The primary contribution of this paper is
59an EDSL based method for translating programs in a
60high level dependently typed programming language to a small core type theory,
61\TT{}, based on UTT \cite{luo1994}. The paper describes the structure of the
62EDSL including proof and system state, and introduces a collection of \remph{tactics}
63for manipulating incomplete programs.
64Secondly, the paper gives a detailed description of the core type theory used
65by \Idris{}, including a full description of the typing rules. Finally, through
66describing the EDSL and the specific tactics, the paper shows how to extend
67\Idris{} with higher level features.
68While we apply these ideas to \Idris{} specifically, the method for term construction
69is equally applicable to other typed programming languages.
71The paper is structured as follows: Section \ref{sect:hll} gives an overview of
72programming in \Idris{}, introducing the high level constructs which will be
73translated to the core language; Section \ref{sect:typechecking} describes the
74core language \TT{} and its typing rules, covering expressions, data types
75and pattern matching; Section \ref{sect:elaboration} describes the method
76for translating \Idris{} to \TT{}, beginning with a restricted language
77\IdrisM{} before extending to higher level features; Section
78\ref{sect:delab} describes the process for translating back to \Idris{}
79and properties of the translation; finally,
80Section \ref{sect:related} discusses related work and Section \ref{sect:conclusion}
83\subsection{Typographical conventions}
85This paper presents programs in two different but related languages: a high level
86language \Idris{} intended for programmers, and a low level language \TT{} to
87which \Idris{} is elaborated. We distinguish these languages typographically as
91\item \Idris{} programs are written in \texttt{typewriter} font, as they are written
92in a conventional text editor. We use \texttt{e$_i$} to stand for non-terminal
94\item \TT{} programs are written in mathematical notation, with names arising
95from \Idris{} expressions written in \texttt{typewriter} font. We use vector notation
96$\te$ to stand for sequences of expressions.
99Additionally, we describe the translation from \Idris{} to \TT{} in the form
100of \emph{meta-operations}, which in practice are Haskell programs. Meta-operations
101are operations on \Idris{} and \TT{} syntax, and are identified by their names being
104\subsection{Elaboration Example}
106\Idris{} is a Haskell-like pure functional programming language with dependent types.
107A simple example program is the following, which adds corresponding elements of
108vectors of the same length:
110\begin{SaveVerbatim}{vadd}
112vAdd : Num a => Vect a n -> Vect a n -> Vect a n
114vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys
120This illustrates some basic features of \Idris{}:
123\item A single colon is used for type declarations, and a double colon for the
125\item Functions are defined by pattern matching, with a top level type declaration.
126Names which are free in the type declaration (\texttt{a} and \texttt{n}) here
128\item The type system ensures that both input vectors are the same length (\texttt{n})
129and have the same element type (\texttt{a}), and that the element type and length
130are preserved in the output vector.
131\item Functions can be overloaded using \remph{type classes}. Here, the element type
132of the vector \texttt{a} must be numeric and therefore supports the \texttt{+} operator.
136\Idris{} programs elaborate into a small core language, \TT{}, which is a $\lambda$-calculus
137with dependent types, augmented with algebraic data types and pattern matching.
138\TT{} programs are fully explicitly typed, including the names \texttt{a} and \texttt{n}
139in the type declaration, and the names bound in each pattern match clause.
140Type classes are also made explicit.
141The \TT{} translation of \texttt{vAdd} is:
146\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to
147 \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\
150\begin{array}{lccccccc}
152\RW{var}\:\va\Hab\Set,\:\vc\Hab\TC{Num}\;\va\SC}\\
153\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\
156\va\Hab\Set,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\
157\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;
158\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk
162\hg\FN{vAdd} & \va & (\suc\;\vk) & \vc
163 & ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
164 & ((\DC{::})\;\va\;\vk\;\vy\;\vys)
166 & & \MRet{5}{((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))}
172The rest of this paper describes \Idris{} and \TT{}, and systematically explains
173how to translate from one to the other.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list