git.iko.soy/Idris-dev
on master help sign in
Abstract
commit9d389c4e935aa2c30dbb50505338d801730d5817 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 7 Apr 2012, 17:58 (15 years ago) parent2899286
2 files changed+38−20
compare with master
unifiedsplit
impl-paper/impldtp.tex+24−8 impl-paper/intro.tex+14−12
impl-paper/impldtp.tex+24−8
@@ -66,14 +66,30 @@ KY16 9SX, UK}
6666\maketitle
6767
6868\begin{abstract}
69−I describe the implementation of a dependently typed functional
70−programming language, \Idris{}. Much has been written about various
71−aspects of dependently typed language implementation (e.g. checking
72−dependent types, unification, optimisation) but nothing yet about how
73−to bring it all together into a complete, practical, usable tool. This paper
74−attempts to do so. In particular, I explain what is needed to turn
75−concrete syntax with implicit arguments into fully elaborated type
76−theory, using unification and a tactic engine.
69+Many components of a dependently typed programming language are by now well
70+understood, such as the underlying type theory, type checking, unification and
71+evaluation. How to combine these components into a realistic and usable high
72+level language is, however, folklore, discovered anew by each succesive
73+language implementations. In this paper, I describe the implementation of a
74+new dependently typed functional programming language, \Idris{}.
75+\Idris{} is intended to be a \emph{general purpose} programming language
76+and as such provides high level concepts such as implicit syntax,
77+type classes and \texttt{do} notation.
78+I describe the high level language and the underlying type theory, and present
79+a method for \emph{elaborating} concrete high level syntax with implicit
80+arguments and type classes into a fully explicit type theory. Furthermore,
81+I show how this method,
82+based on a domain specific language embedded in Haskell, facilitates the
83+implementation of new high level language constructs.
84+
85+%I describe the implementation of a dependently typed functional
86+%programming language, \Idris{}. Much has been written about various
87+%aspects of dependently typed language implementation (e.g. checking
88+%dependent types, unification, optimisation) but nothing yet about how
89+%to bring it all together into a complete, practical, usable tool. This paper
90+%attempts to do so. In particular, I explain what is needed to turn
91+%concrete syntax with implicit arguments into fully elaborated type
92+%theory, using unification and a tactic engine.
7793\end{abstract}
7894
7995%\category{D.3.2}{Programming Languages}{Language
impl-paper/intro.tex+14−12
@@ -4,43 +4,45 @@ Dependently typed programming languages, such as Agda \cite{norell2007thesis}
44and Coq \cite{Bertot2004}, have emerged in recent years as a promising approach
55to ensuring the correctness of software. The \Idris{} language
66\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,
88which have arisen from the theorem proving community, \Idris{} takes Haskell as
9−its baseline. Recent Haskell extensions such as GADTs and type families have
10−given some of the power of dependent types to Haskell programmers. However,
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. 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,
1114these 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
1316language, has no such limitation, essentially asking the question:
1417
1518\begin{center}
1619\emph{``What if Haskell had \emph{full} dependent types?''}
1720\end{center}
1821
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
2023a notation which allows programmers to express high level concepts
2124in a natural way. Taking Haskell as a starting point means that \Idris{} offers
2225high level structures such as type classes, \texttt{do}-notation, primitive types
2326and monadic I/O, for example.
2427Nevertheless, it is important for the sake of correctness of the language implementation
2528to have a small core language with well understood meta-theory
26−\cite{Altenkirch2010}.
27−
29+\cite{Altenkirch2010}.
2830How can we achieve both of these goals?
2931
3032This paper describes a method for elaborating a high level dependently typed
3133functional programming language to a low level core language based on dependent
3234type theory. The method involves building an Embedded Domain Specific Language
3335(EDSL) for constructing programs in the core language, using \emph{tactics}
34−directed by high level
35−program syntax.
36−%This method allows higher level language constructs to be
37−%constructed in a straightforward manner.
36+directed by high level program syntax.
37+As we shall see, this method allows higher level language constructs to be
38+constructed in a straightforward manner, without compromising the simplicity
39+of the underlying type theory.
3840
3941\subsection{Overview}
4042
4143A dependently typed programming language relies on several components, many of
4244which 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
4446unification algorithm \cite{Miller1992} and an evaluator. However, it is less
4547well understood how to combine these components effectively into a practical
4648programming language. Therefore, the primary contribution of this paper is