git.iko.soy/Idris-dev
on master help sign in
typos again
d9516efEdwin Brady
impl-paper/hll.tex+1−1
compare with master
unifiedsplit
@@ -350,7 +350,7 @@ where the name suggests the argument's purpose.
350\subsection{Type Classes}
350\subsection{Type Classes}
351
351
352\Idris{} supports overloading in two ways. Firstly, as we have already seen with
352\Idris{} supports overloading in two ways. Firstly, as we have already seen with
353−this constructors of \texttt{List} and \texttt{Vect}, names
353+the constructors of \texttt{List} and \texttt{Vect}, names
354can be overloaded in an ad-hoc manner and resolved according to the context in which
354can be overloaded in an ad-hoc manner and resolved according to the context in which
355they are used. This is mostly for convenience, to eliminate the need to decorate
355they are used. This is mostly for convenience, to eliminate the need to decorate
356constructor names in similarly structured data types, and eliminate explicit qualification
356constructor names in similarly structured data types, and eliminate explicit qualification
impl-paper/library.bib+21−21
@@ -1,20 +1,12 @@
1Automatically generated by Mendeley 1.3.1
1Automatically generated by Mendeley 1.3.1
2Any changes to this file will be lost if it is regenerated by Mendeley.
2Any changes to this file will be lost if it is regenerated by Mendeley.
3
3
4−@inproceedings{Altenkirch2010,
4+@article{McBride2006,
5−abstract = {The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs. To address these issues we introduce $\Pi$$\Sigma$, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursionused for types, functions and infinite objectsand an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of $\alpha$-equality for recursive definitions. We show, by translating several high-level constructions, that $\Pi$$\Sigma$ is suitable as a core language for dependently typed programming.},
5+author = {McBride, C and Goguen, H and McKinna, J},
6−author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
6+journal = {Types for Proofs and Programs},
7−booktitle = {{FLOPS 2010}},
7+title = {{A few constructions on constructors}},
8−doi = {10.1007/978-3-642-12251-4_5},
9−editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
10−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
11−isbn = {9783642122507},
12−pages = {40----55},
13−publisher = {Springer Berlin Heidelberg},
14−series = {Lecture Notes in Computer Science},
15−title = {{Dependent Types without the Sugar}},
16−url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
8+url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
17−year = {2010}
9+year = {2006}
18}
10}
19@inproceedings{ko2011modularising,
11@inproceedings{ko2011modularising,
20author = {Ko, H.S. and Gibbons, J.},
12author = {Ko, H.S. and Gibbons, J.},
@@ -464,6 +456,21 @@ title = {{Typing Haskell in Haskell}},
464url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
456url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
465year = {1999}
457year = {1999}
466}
458}
459+@inproceedings{Altenkirch2010,
460+abstract = {The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs. To address these issues we introduce $\Pi$$\Sigma$, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursionused for types, functions and infinite objectsand an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of $\alpha$-equality for recursive definitions. We show, by translating several high-level constructions, that $\Pi$$\Sigma$ is suitable as a core language for dependently typed programming.},
461+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
462+booktitle = {{FLOPS 2010}},
463+doi = {10.1007/978-3-642-12251-4_5},
464+editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
465+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
466+isbn = {9783642122507},
467+pages = {40----55},
468+publisher = {Springer Berlin Heidelberg},
469+series = {Lecture Notes in Computer Science},
470+title = {{Dependent Types without the Sugar}},
471+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
472+year = {2010}
473+}
467@book{Bertot2004,
474@book{Bertot2004,
468author = {Bertot, Yves and Cast\'{e}ran, Pierre},
475author = {Bertot, Yves and Cast\'{e}ran, Pierre},
469publisher = {Springer},
476publisher = {Springer},
@@ -785,13 +792,6 @@ url = {http://dl.acm.org/citation.cfm?id=1707801.1706350},
785volume = {45},
792volume = {45},
786year = {2010}
793year = {2010}
787}
794}
788−@article{McBride2006,
789−author = {McBride, C},
790−journal = {Types for Proofs and Programs},
791−title = {{A few constructions on constructors}},
792−url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
793−year = {2006}
794−}
795@inproceedings{coquand1986analysis,
795@inproceedings{coquand1986analysis,
796author = {Coquand, T.},
796author = {Coquand, T.},
797booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},
797booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},
impl-paper/typechecking.tex+2−2
@@ -412,7 +412,7 @@ with the next clause. The algorithm uses the following meta-operations:
412\item $\MO{Con}\:\vx$, which returns true if $\vx$ is a constructor name
412\item $\MO{Con}\:\vx$, which returns true if $\vx$ is a constructor name
413\item $\MO{Arity}\:\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
413\item $\MO{Arity}\:\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
414$\vx$ requires.
414$\vx$ requires.
415−\item $\MO{Length}\:\tts$, which returns the length of the telescope $\tts$
415+\item $\MO{Length}\:\tts$, which returns the length of the vector $\tts$
416\end{itemize}
416\end{itemize}
417
417
418
418
@@ -456,7 +456,7 @@ $\vx$ requires.
456{pmatch}
456{pmatch}
457
457
458By convention, we write the application of a meta-operation $\MO{Op}$
458By convention, we write the application of a meta-operation $\MO{Op}$
459−to a telescope $\tx$ as $\vec{\MO{Op}}\:\tx$.
459+across a vector $\tx$ as $\vec{\MO{Op}}\:\tx$.
460In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
460In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
461a tree of case expressions~\cite{Augustsson1985}.
461a tree of case expressions~\cite{Augustsson1985}.
462
462