5Dependently typed programming languages have becoming more prominent in recent
6years as tools for verifying software correctness, and several experimental
7languages are being developed, in particular Agda \cite{norell2007thesis}, Epigram
8\cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.
10An earlier implementation of \Idris{} was built on the \Ivor{} proof engine
11\cite{Brady2006b}. This implementation differed in one important way --- unlike
12the present implementation, there was limited separation between the type theory
13and the high level language. The type theory itself supported implicit syntax and
14unification, with high level constructs such as the \texttt{with} rule implemented
15directly. Two important disadvantages were found with this approach, however:
16firstly, the type checker is much more complicated when combined with
17unification, making it harder to maintain; secondly, adding new high level features
18requires the type checker to support those features directly. In contrast, elaboration
19by tactics gives a clean separation between the low level and high level languages.
21The Agda implementation is based on a type theory with
22implicit syntax and pattern matching --- Norell gives an algorithm for type checking
23a dependently typed language with pattern matching and metavariables
24\cite{norell2007thesis}. Unlike the present \Idris{} implementation, metavariables
25and implicit arguments are part of the type theory. This has the advantage that
26implicit arguments can be used more freely, at the expense of complicating the type
29Epigram \cite{McBride2004a} and Oleg \cite{McBride1999}
30have provided much of the inspiration for the \Idris{} elaborator. Indeed,
31the hole and guess bindings of \TTdev{} are taken directly from Oleg.
32\Epigram{} does not implement pattern matching directly, but rather translates
33pattern matching into elimination rules \cite{McBride2002}. This has the
35elimination rules provide termination and coverage proofs \emph{by construction}.
36Furthermore they simplify implementation of the evaluator and provide easy
37optimisation opportunities \cite{Brady2003}. However, it requires the
38implementation of extra machinery for constructor manipulation
39\cite{McBride2006} and so we have avoided it in the present implementation.
41%Comparison with GHC's type system and type checker. \cite{Vytiniotis2011}
43%[Observation: separate elaboration and type checking, sort of like in GHC which
44%type checks the high level language and produces a type correct core language.
45%Elaboration is effectively a type checker for the high level language, so we have
46%a hope of providing reasonable error messages related to the original code.]
50\label{sect:conclusion}
52In this paper, I have given an overview of the programming language \Idris{},
53and its core type theory \TT{}, giving a detailed algorithm for translating
54high level programs into \TT{}.
55\TT{} itself is deliberately small and simple, and the design has deliberately
56resisted innovation so that we can rely on existing metatheoretic properties
57being preserved. The kernel of the \Idris{} implementation consists of a type checker
58and evaluator for \TT{} along with a pattern match compiler, which are implemented
59in under 1000 lines of Haskell code. It is important that this kernel remains small
60--- the correctness of the language implementation relies to a large extent on
61the correctness of the underlying type system, and keeping the implementation small
62reduces the possibility of errors.
64The approach we have taken to implementing the high level language, implementing
65a tactic language as an embedded DSL, allows us to
66build programs on top of a small and unchanging kernel, rather than extending
67the core language to deal with implicit syntax, unification and type classes.
68High level \Idris{} features are implemented by describing the corresponding
69sequence of tactics to build an equivalent program in \TT{}, via a development
70calculus of incomplete terms, \TTdev{}. A significant advantage we have found with
71this approach is that higher level features can easily be implemented in terms
72of existing elaborator components. For example, once we have implemented elaboration
73for data types and functions, it is easy to add several features:
76\item \textbf{Type classes}: A dictionary is merely a record containing the
77functions which implement a type class instance. Since we have a tactic based
78refinement engine, we can implement type class resolution as a tactic.
79\item \textbf{\texttt{where} clauses}: We have access to local variables and
81elaborate \texttt{where} clauses at the point of definition simply by lifting
83\item \textbf{\texttt{case} expressions}: Similar to \texttt{where} clauses,
84these are implemented by lifting the branches out to a top level function.
87We do not need to make any changes to the core language type system in order to
88implement these high level features.
89Other high level features such as dependent records, tuples and monad comprehensions
90can be added equally easily. Furthermore,
91since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it is
92possible to expose the tactic language to the programmer. This opens up the
93possibility of implementing domain specific decision procedures, or implementing
94user defined tactics in a style similar to Coq's \texttt{Ltac} language \cite{Delahaye2000}.
95Although \TT{} is primarily intended as a core language for \Idris{},
96its rich type system also allows it to capture a number of high level languages, especially
97when augmented with primitive operators.
99We have not discussed the performance of the elaboration
100algorithm, or described how \Idris{} compiles to executable code. In practice,
101we have found performance to be acceptable --- for example, the \Idris{}
102library (25 files, 3532 lines of code in total at the time of writing)
103elaborates in around 10 seconds\footnote{On a MacBook Pro, 2.8GHz Intel Core 2
104Duo, 4Gb RAM}. Profiling suggests that the main bottleneck is locating holes
105in a proof term, which can be improved by choosing a better representation
106for proof terms, perhaps based on a zipper \cite{Huet1997}. Compilation is made
107straightforward by the Epic library \cite{brady2011epic}, with I/O and foreign
108functions handled using command-response interaction trees \cite{Hancock2000}.
110The objective of this implementation of \Idris{} is to provide a platform
111for experimenting with realistic, general purpose programming with dependent
112types, by implementing a Haskell-like language augmented with \emph{full}
114In this paper, we have seen how such a high level language can be implemented
115by building on top of a small, well-understood, easy to reason about type
117However, a programming language implementation is not an end in itself.
118Programming languages exist to support research and practice in many different
119domains. In future work, therefore, we plan to apply domain specific
120language based techniques to realistic problems
121in important safety critical domains such as security and network protocol
122design and implementation. In order to be successful, we need a language which
123is expressive enough to describe protocol specifications at a high level, and robust
124enough to guarantee correct implementation of those protocols. \Idris{}, we believe,
125is the right tool for this work.
129%\subsection{Further Work}
131%[Would the EDSL approach work in other languages? Adding components of DTP
132%to imperative languages, say, using \TT{} as a verified core.
133%\Idris{} implementation as the beginning of a project to explore practical
134%DTP --- systems, protocols, security especially. And just having full
135%dependent types for lightweight correctness guarantees.]
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