git.iko.soy/Idris-dev
on da8d396 help sign in
Idris-dev/papers/impl-paper/impldtp.tex
159 lines 4.6 kB history raw
1\RequirePackage{amsmath}
2\documentclass{jfp1}
3%\documentclass[acmtoplas]{acmtrans2m}
5\usepackage[draft]{comments}
6%\usepackage[final]{comments}
7% \newcommand{\comment}[2]{[#1: #2]}
8\newcommand{\khcomment}[1]{\comment{KH}{#1}}
9\newcommand{\ebcomment}[1]{\comment{EB}{#1}}
11\usepackage{epsfig}
12%\usepackage{path}
13\usepackage{url}
14\usepackage{fancyvrb}
16\newenvironment{template}{\sffamily}
18%\usepackage{graphics,epsfig}
19\usepackage{stmaryrd}
20\usepackage{amsmath}
22\input{./macros.ltx}
23\input{./library.ltx}
25\NatPackage
26\FinPackage
28\newcounter{per}
29\setcounter{per}{1}
31\newcommand{\Ivor}{\textsc{Ivor}}
32\newcommand{\Idris}{\textsc{Idris}}
33\newcommand{\IdrisM}{\textsc{Idris}$^-$}
34\newcommand{\TT}{\textsf{TT}}
35\newcommand{\TTdev}{\textsf{TT$_{dev}$}}
36\newcommand{\Funl}{\textsc{Funl}}
37\newcommand{\Agda}{\textsc{Agda}}
38\newcommand{\LamPi}{$\lambda_\Pi$}
40\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
41\begin{center}
42\fbox{
43\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
44\end{minipage}}
45\end{center}
46\vspace*{0.1cm}
49\newcommand{\mysubsubsection}[1]{
50\noindent
51\textbf{#1}
53\newcommand{\hdecl}[1]{\texttt{#1}}
56\title
57[Idris, a General Purpose Dependently Typed Programming Language]
58{Idris, a General Purpose Dependently Typed Programming Language:
59Design and Implementation}
60%Implementing General Purpose Dependently Typed Programming Languages}
61%\subtitle{Implementing Domain Specific Languages by Overloading}
63\author[Edwin Brady]
64{EDWIN BRADY\\
65School of Computer Science, University of St Andrews, St Andrews,
66KY16 9SX, UK}
68\begin{document}
70\maketitle
72\begin{abstract}
73Many components of a dependently-typed programming language are by now well
74understood, for example the underlying type theory, type checking, unification and
75evaluation. How to combine these components into a realistic and usable
76high-level language is, however, folklore, discovered anew by successive
77language implementators. In this paper, I describe the implementation of
78\Idris{}, a new dependently-typed functional programming language.
79\Idris{} is intended to be a \emph{general purpose} programming language
80and as such provides high-level concepts such as implicit syntax,
81type classes and \texttt{do} notation.
82I describe the high-level language and the underlying type theory, and present
83a tactic-based method for \emph{elaborating} concrete high-level syntax with
84implicit arguments and type classes into a fully explicit type theory.
85Furthermore, I show how this method facilitates the implementation of new
86high-level language constructs.
88%I describe the implementation of a dependently typed functional
89%programming language, \Idris{}. Much has been written about various
90%aspects of dependently typed language implementation (e.g. checking
91%dependent types, unification, optimisation) but nothing yet about how
92%to bring it all together into a complete, practical, usable tool. This paper
93%attempts to do so. In particular, I explain what is needed to turn
94%concrete syntax with implicit arguments into fully elaborated type
95%theory, using unification and a tactic engine.
96\end{abstract}
99%\category{D.3.2}{Programming Languages}{Language
100% Classifications}[Applicative (functional) Languages]
101%\category{D.3.4}{Programming Languages}{Processors}[Compilers]
102%\terms{Languages, Verification, Performance}
103%\keywords{Dependent Types, Typechecking}
106%\begin{bottomstuff}
107%Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
108%KY16 9SX
109%\end{bottomstuff}
111\input{intro.tex}
113%\input{overview.tex}
115\input{hll.tex}
117\input{typechecking.tex}
119%\input{proofstate.tex}
121\input{elaboration.tex}
123\input{delab.tex}
125%\input{compiling.tex}
127%\input{syntax.tex}
129\input{conclusions.tex}
131\section*{Acknowledgements}
133This work was funded by the Scottish Informatics and Computer Science Alliance
134(SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE). My thanks to
135Philip H\"{o}lzenspies, Kevin Hammond, Vilhelm Sj\"{o}berg, Falko Spiller
136and Nathan Collins
137for their comments on an earlier draft of this paper, and to the anonymous
138referees for their many insightful and constructive comments.
140\bibliographystyle{jfp}
141\bibliography{library.bib}
143\appendix
145%\section{TODOs}
146%\listoftodos{}
148%\section{Elaboration meta-operations}
150%It's possible that it would be useful to have a quick reference of meta-operations
151%used by the elaborator here.
153%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
154%$\MO{NewProof}$, $\MO{NewTerm}$,
155%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.
157%\input{code}
159\end{document}