Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

156 lines (114 sloc) 4.534 kB
% \newcommand{\comment}[2]{[#1: #2]}
\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
{Implementing General Purpose Dependently Typed Programming Languages}
%\subtitle{Implementing Domain Specific Languages by Overloading}
\author[Edwin Brady]
School of Computer Science, University of St Andrews, St Andrews,
KY16 9SX, UK}
Many components of a dependently typed programming language are by now well
understood, for example the underlying type theory, type checking, unification and
evaluation. How to combine these components into a realistic and usable high
level language is, however, folklore, discovered anew by successive
language implementations. In this paper, I describe the implementation of a
new dependently typed functional programming language, \Idris{}.
\Idris{} is intended to be a \emph{general purpose} programming language
and as such provides high level concepts such as implicit syntax,
type classes and \texttt{do} notation.
I describe the high level language and the underlying type theory, and present
a method for \emph{elaborating} concrete high level syntax with implicit
arguments and type classes into a fully explicit type theory. Furthermore,
I show how this method,
based on a domain specific language embedded in Haskell, facilitates the
implementation of new high level language constructs.
%I describe the implementation of a dependently typed functional
%programming language, \Idris{}. Much has been written about various
%aspects of dependently typed language implementation (e.g. checking
%dependent types, unification, optimisation) but nothing yet about how
%to bring it all together into a complete, practical, usable tool. This paper
%attempts to do so. In particular, I explain what is needed to turn
%concrete syntax with implicit arguments into fully elaborated type
%theory, using unification and a tactic engine.
%\category{D.3.2}{Programming Languages}{Language
% Classifications}[Applicative (functional) Languages]
%\category{D.3.4}{Programming Languages}{Processors}[Compilers]
%\terms{Languages, Verification, Performance}
%\keywords{Dependent Types, Typechecking}
%Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
%KY16 9SX
This work was funded by the Scottish Informatics and Computer Science
Alliance (SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE).
My thanks to Kevin Hammond and Vilhelm Sj\"{o}berg for their comments
on an earlier draft of this paper.
%\section{Elaboration meta-operations}
%It's possible that it would be useful to have a quick reference of meta-operations
%used by the elaborator here.
%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
%$\MO{NewProof}$, $\MO{NewTerm}$,
%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.
Jump to Line
Something went wrong with that request. Please try again.