091a5df · Idris-dev · git.iko.soy

papers/impl-paper/conclusions.tex+5−1

compare with master

unifiedsplit

@@ -45,7 +45,7 @@ Matita uses a bi-directional refinement algorithm~\cite{Asperti}. This is a

45type directed approach, maintaining a set of yet to be solved unification

46problems and relying on a small kernel, similar to the approach we now take

47with \Idris{}, However, their approach uses refinement rules rather than

48−actics. This leads to good error messages though it is not clear how

48+tactics. This leads to good error messages though it is not clear how

49easy it would be to extend to additional high level language features, unlike

50the tactic based approach.

51

@@ -141,6 +141,10 @@ in a proof term, which can be improved by choosing a better representation

141for proof terms, perhaps based on a zipper \cite{Huet1997}. Compilation is made

142straightforward by the Epic library \cite{brady2011epic}, with I/O and foreign

143functions handled using command-response interaction trees \cite{Hancock2000}.

144+Although we have not yet run detailed benchmarks of the performance of compiled

145+code, we believe that rich type information and guaranteed termination will

146+allow aggressive optimisations~\cite{Brady2003,Brady2005}. We will investigate

147+this in future work.

144

148

145The objective of this implementation of \Idris{} is to provide a platform

149The objective of this implementation of \Idris{} is to provide a platform

146for experimenting with realistic, general purpose programming with dependent

150for experimenting with realistic, general purpose programming with dependent

papers/impl-paper/elaboration.tex+2−2

@@ -131,7 +131,7 @@ either indicates success, or reports an error $\MO{Err}$:

131}

132

133\noindent

134−If any operation fails during a proof (e.g. a subterm fails to type check)

134+If any operation fails during a proof (e.g. a sub term fails to type check)

135then the entire proof fails (i.e. returns $\MO{Failure}\;\ve$ with some error

136message $\ve$) unless otherwise handled.

137

@@ -1050,7 +1050,7 @@ has already been set up, which means that elaboration can always be

1050\remph{type-directed} since the proof state contains the type of the expression we

1051are building.

1052

1053−In all cases except the elaboration of variables and constantes,

1053+In all cases except the elaboration of variables and constants,

1054$\ttpinterp{\vx}\;=\;\ttinterp{\vx}$.

1055

1056\subsubsection{Elaborating variables and constants}

papers/impl-paper/hll.tex+1−1

@@ -377,7 +377,7 @@ by translating functions to eliminators~\cite{McBride2004a} we have taken

377the more pragmatic approach of allowing more flexibility for the programmer

378at the expense of simplicity of totality checking. \Idris{} also supports

379coinductive definitions with a corresponding productivity checker, although

380−futher details are beyond the scope of this paper.

380+further details are beyond the scope of this paper.

381

382\subsection{Type Classes}

383

papers/impl-paper/intro.tex+5−5

@@ -38,10 +38,10 @@ well-defined core language with well-understood meta-theory \cite{Altenkirch2010

38How can we achieve both of these goals?

39

40This paper describes a method for elaborating a high level dependently typed

41−functional programming language to a low level core language based on dependent

41+functional programming language to a low level core based on dependent

42type theory. The method involves building an elaboration monad which captures

43the state of incomplete programs and a collection of \emph{tactics} for

44−refining programs, directed by high level program syntax. As we shall see,

44+refining programs, directed by high level syntax. As we shall see,

45this method allows higher level language constructs to be constructed in a

46straightforward manner, without compromising the simplicity of the underlying

47type theory.

@@ -103,9 +103,9 @@ in $\MO{SmallCaps}$.

103

104\subsection{Elaboration Example}

105

106−\Idris{} is a Haskell-like pure functional programming language with dependent types.

106+\Idris{} is a Haskell-like pure functional programming language with dependent

107−A simple example program is the following, which adds corresponding elements of

107+types. A simple example program is the following, which adds corresponding

108−vectors of the same length:

108+elements of vectors of the same length:

109

110\begin{SaveVerbatim}{vadd}

111

papers/impl-paper/typechecking.tex+1−1

@@ -523,7 +523,7 @@ Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property

523\demph{subject reduction} (i.e. that computation preserves type); the

524\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into

525their scope); and \demph{strengthening} (i.e. that removing unused definitions

526−from scope does not affect typechecking).

526+from scope does not affect type checking).

527

528One property which is noticeably absent is \demph{strong normalisation}.

529Although desirable to preserve termination and decidability of type checking,