git.iko.soy/Idris-dev
on master help sign in
Some polishing, spell checking
commit091a5df3b8bd7379fe287372165469230e09672e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 15 Feb 2013, 12:38 (14 years ago) parent99bc1d5
5 files changed+14−10
compare with master
unifiedsplit
papers/impl-paper/conclusions.tex+5−1 papers/impl-paper/elaboration.tex+2−2 papers/impl-paper/hll.tex+1−1 papers/impl-paper/intro.tex+5−5 papers/impl-paper/typechecking.tex+1−1
papers/impl-paper/conclusions.tex+5−1
@@ -45,7 +45,7 @@ Matita uses a bi-directional refinement algorithm~\cite{Asperti}. This is a
4545type directed approach, maintaining a set of yet to be solved unification
4646problems and relying on a small kernel, similar to the approach we now take
4747with \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
4949easy it would be to extend to additional high level language features, unlike
5050the tactic based approach.
5151
@@ -141,6 +141,10 @@ in a proof term, which can be improved by choosing a better representation
141141for proof terms, perhaps based on a zipper \cite{Huet1997}. Compilation is made
142142straightforward by the Epic library \cite{brady2011epic}, with I/O and foreign
143143functions 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.
144148
145149The objective of this implementation of \Idris{} is to provide a platform
146150for 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}$:
131131}
132132
133133\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)
135135then the entire proof fails (i.e. returns $\MO{Failure}\;\ve$ with some error
136136message $\ve$) unless otherwise handled.
137137
@@ -1050,7 +1050,7 @@ has already been set up, which means that elaboration can always be
10501050\remph{type-directed} since the proof state contains the type of the expression we
10511051are building.
10521052
1053−In all cases except the elaboration of variables and constantes,
1053+In all cases except the elaboration of variables and constants,
10541054$\ttpinterp{\vx}\;=\;\ttinterp{\vx}$.
10551055
10561056\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
377377the more pragmatic approach of allowing more flexibility for the programmer
378378at the expense of simplicity of totality checking. \Idris{} also supports
379379coinductive 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.
381381
382382\subsection{Type Classes}
383383
papers/impl-paper/intro.tex+5−5
@@ -38,10 +38,10 @@ well-defined core language with well-understood meta-theory \cite{Altenkirch2010
3838How can we achieve both of these goals?
3939
4040This 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
4242type theory. The method involves building an elaboration monad which captures
4343the 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,
4545this method allows higher level language constructs to be constructed in a
4646straightforward manner, without compromising the simplicity of the underlying
4747type theory.
@@ -103,9 +103,9 @@ in $\MO{SmallCaps}$.
103103
104104\subsection{Elaboration Example}
105105
106−\Idris{} is a Haskell-like pure functional programming language with dependent types.
107−A simple example program is the following, which adds corresponding elements of
108−vectors of the same length:
106+\Idris{} is a Haskell-like pure functional programming language with dependent
107+types. A simple example program is the following, which adds corresponding
108+elements of vectors of the same length:
109109
110110\begin{SaveVerbatim}{vadd}
111111
papers/impl-paper/typechecking.tex+1−1
@@ -523,7 +523,7 @@ Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property
523523\demph{subject reduction} (i.e. that computation preserves type); the
524524\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into
525525their 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).
527527
528528One property which is noticeably absent is \demph{strong normalisation}.
529529Although desirable to preserve termination and decidability of type checking,