git.iko.soy/Idris-dev
on master help sign in
More on related work
commitfe89d0dc0ad48f04a8284cacd195d83483231663 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 10 Feb 2013, 11:58 (14 years ago) parent8843539
2 files changed+43−25
compare with master
unifiedsplit
papers/impl-paper/conclusions.tex+23−5 papers/impl-paper/library.bib+20−20
papers/impl-paper/conclusions.tex+23−5
@@ -6,9 +6,28 @@ Dependently typed programming languages have becoming more prominent in recent
66years as tools for verifying software correctness, and several experimental
77languages are being developed, in particular Agda \cite{norell2007thesis},
88Epigram \cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.
9−The problem of refining high level syntax to a core type theory also applies
10−to theorem provers based on dependent types such as Coq~\cite{Bertot2004}
11−and Matita~\cite{Asperti2011}.
9+Furthermore, recent extensions to Haskell~\cite{Haskell98}, implemented in the
10+Glasgow Haskell Compiler, are bringing more of the power of dependent types to
11+Haskell. The problem of refining high level syntax to a core type theory also
12+applies to theorem provers based on dependent types such as
13+Coq~\cite{Bertot2004} and Matita~\cite{Asperti2011}.
14+
15+Checking advanced type system features in Haskell involves a type system
16+parameterised over an underlying constraint system $X$ which captures
17+constraints such as type classes, constrained data types and type families.
18+Types are checked using an inference algorithm
19+\textsc{OutsideIn(X)}~\cite{Vytiniotis2011}, which is stratified into an
20+inference engine independent of the constraint
21+system, and a constraint solver for $X$. An additional difficulty faced by
22+Haskell, and hence any extensions, is the desire to support type \emph{inference}, in
23+which principal types may be inferred for top level functions. We have avoided
24+such difficulties since, in general, type
25+inference is undecidable for full dependent types. Indeed, it is not clear
26+that type inference is even desirable in many cases, as programmers
27+can use dependent types to state their intentions (hence a program
28+specification) more precisely. However in future work we
29+may consider adapting the \textsc{OutsideIn} approach to provide limited type
30+inference.
1231
1332An earlier implementation of \Idris{} was built on the \Ivor{} proof engine
1433\cite{Brady2006b}. This implementation differed in one important way --- unlike
@@ -29,7 +48,6 @@ with \Idris{}, However, their approach uses refinement rules rather than
2948actics. This leads to good error messages though it is not clear how
3049easy it would be to extend to additional high level language features, unlike
3150the tactic based approach.
32−Similarly, the new GHC type checker~\cite{Vytiniotis2011} \ldots \textbf{TODO}
3351
3452The Agda implementation is based on a type theory with
3553implicit syntax and pattern matching --- Norell gives an algorithm for type checking
@@ -51,7 +69,7 @@ optimisation opportunities \cite{Brady2003}. However, it requires the
5169implementation of extra machinery for constructor manipulation
5270\cite{McBride2006} and so we have avoided it in the present implementation.
5371
54−%Comparison with GHC's type system and type checker. \cite{Vytiniotis2011}
72+
5573
5674%[Observation: separate elaboration and type checking, sort of like in GHC which
5775%type checks the high level language and produces a type correct core language.
papers/impl-paper/library.bib+20−20
@@ -1,13 +1,18 @@
11Automatically generated by Mendeley 1.6
22Any changes to this file will be lost if it is regenerated by Mendeley.
33
4−@inproceedings{Asperti2011,
5−author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},
6−booktitle = {Automated Deduction --- CADE-23},
7−file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/The Matita Interactive Theorem Prover/Asperti et al. - The Matita Interactive Theorem Prover - 2011.pdf:pdf},
8−pages = {64----69},
9−title = {{The Matita Interactive Theorem Prover}},
10−year = {2011}
4+@techreport{Haskell98,
5+abstract = {Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support Haskell 98, so professioanls and educators have a stable base for their work.},
6+author = {{Peyton Jones}, Simon},
7+booktitle = {Language},
8+editor = {Jones, Simon Peyton},
9+isbn = {0521826144},
10+number = {1},
11+publisher = {Cambridge University Press},
12+title = {{Haskell 98 Language and Libraries: The Revised Report}},
13+url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&amp;path=ASIN/0521826144},
14+volume = {13},
15+year = {2002}
1116}
1217@inproceedings{McBride2006,
1318author = {McBride, C and Goguen, H and McKinna, J},
@@ -141,19 +146,6 @@ author = {Walt, Paul Van Der and Swierstra, Wouter},
141146file = {:Users/edwin/Documents/Mendeley Desktop/Walt, Swierstra/Engineering Proof by Reflection in Agda/Walt, Swierstra - Engineering Proof by Reflection in Agda - Unknown.pdf:pdf},
142147title = {{Engineering Proof by Reflection in Agda}}
143148}
144−@article{Jones2003,
145−abstract = {Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support Haskell 98, so professioanls and educators have a stable base for their work.},
146−author = {Jones, Simon Peyton},
147−editor = {Jones, Simon Peyton},
148−isbn = {0521826144},
149−journal = {Language},
150−number = {1},
151−publisher = {Cambridge University Press},
152−title = {{Haskell 98 Language and Libraries The Revised Report}},
153−url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&amp;path=ASIN/0521826144},
154−volume = {13},
155−year = {2003}
156−}
157149@inproceedings{madhavapeddy2007melange,
158150author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},
159151booktitle = {ACM SIGOPS Operating Systems Review},
@@ -1287,6 +1279,14 @@ url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},
12871279volume = {32},
12881280year = {1989}
12891281}
1282+@inproceedings{Asperti2011,
1283+author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},
1284+booktitle = {Automated Deduction --- CADE-23},
1285+file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/The Matita Interactive Theorem Prover/Asperti et al. - The Matita Interactive Theorem Prover - 2011.pdf:pdf},
1286+pages = {64----69},
1287+title = {{The Matita Interactive Theorem Prover}},
1288+year = {2011}
1289+}
12901290@article{Brady2006a,
12911291author = {Brady, E and Hammond, K},
12921292file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/A verified staged interpreter is a verified compiler/Brady, Hammond - A verified staged interpreter is a verified compiler - 2006.pdf:pdf},