fe89d0d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More on related work

fe89d0dEdwin Brady14 years ago

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

compare with master

unifiedsplit

@@ -6,9 +6,28 @@ Dependently 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},

8Epigram \cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.

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

9−The problem of refining high level syntax to a core type theory also applies

11+Haskell. The problem of refining high level syntax to a core type theory also

10−to theorem provers based on dependent types such as Coq~\cite{Bertot2004}

12+applies to theorem provers based on dependent types such as

11−and Matita~\cite{Asperti2011}.

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.

13An earlier implementation of \Idris{} was built on the \Ivor{} proof engine

32An earlier implementation of \Idris{} was built on the \Ivor{} proof engine

14\cite{Brady2006b}. This implementation differed in one important way --- unlike

33\cite{Brady2006b}. This implementation differed in one important way --- unlike

@@ -29,7 +48,6 @@ with \Idris{}, However, their approach uses refinement rules rather than

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

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

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

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

31the tactic based approach.

50the tactic based approach.

32−Similarly, the new GHC type checker~\cite{Vytiniotis2011} \ldots \textbf{TODO}

34The Agda implementation is based on a type theory with

52The Agda implementation is based on a type theory with

35implicit syntax and pattern matching --- Norell gives an algorithm for type checking

53implicit syntax and pattern matching --- Norell gives an algorithm for type checking

@@ -51,7 +69,7 @@ optimisation opportunities \cite{Brady2003}. However, it requires the

51implementation of extra machinery for constructor manipulation

69implementation of extra machinery for constructor manipulation

52\cite{McBride2006} and so we have avoided it in the present implementation.

70\cite{McBride2006} and so we have avoided it in the present implementation.

54−%Comparison with GHC's type system and type checker. \cite{Vytiniotis2011}

72+

56%[Observation: separate elaboration and type checking, sort of like in GHC which

74%[Observation: separate elaboration and type checking, sort of like in GHC which

57%type checks the high level language and produces a type correct core language.

75%type checks the high level language and produces a type correct core language.

papers/impl-paper/library.bib+20−20

@@ -1,13 +1,18 @@

1Automatically generated by Mendeley 1.6

2Any changes to this file will be lost if it is regenerated by Mendeley.

4−@inproceedings{Asperti2011,

4+@techreport{Haskell98,

5−author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},

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−booktitle = {Automated Deduction --- CADE-23},

6+author = {{Peyton Jones}, Simon},

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},

7+booktitle = {Language},

8−pages = {64----69},

8+editor = {Jones, Simon Peyton},

9−title = {{The Matita Interactive Theorem Prover}},

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&path=ASIN/0521826144},

14+volume = {13},

10−year = {2011}

15+year = {2002}

11}

16}

12@inproceedings{McBride2006,

17@inproceedings{McBride2006,

13author = {McBride, C and Goguen, H and McKinna, J},

18author = {McBride, C and Goguen, H and McKinna, J},

@@ -141,19 +146,6 @@ author = {Walt, Paul Van Der and Swierstra, Wouter},

141file = {:Users/edwin/Documents/Mendeley Desktop/Walt, Swierstra/Engineering Proof by Reflection in Agda/Walt, Swierstra - Engineering Proof by Reflection in Agda - Unknown.pdf:pdf},

146file = {:Users/edwin/Documents/Mendeley Desktop/Walt, Swierstra/Engineering Proof by Reflection in Agda/Walt, Swierstra - Engineering Proof by Reflection in Agda - Unknown.pdf:pdf},

142title = {{Engineering Proof by Reflection in Agda}}

147title = {{Engineering Proof by Reflection in Agda}}

143}

148}

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&path=ASIN/0521826144},

154−volume = {13},

155−year = {2003}

156−}

157@inproceedings{madhavapeddy2007melange,

149@inproceedings{madhavapeddy2007melange,

158author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},

150author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},

159booktitle = {ACM SIGOPS Operating Systems Review},

151booktitle = {ACM SIGOPS Operating Systems Review},

@@ -1287,6 +1279,14 @@ url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},

1287volume = {32},

1279volume = {32},

1288year = {1989}

1280year = {1989}

1289}

1281}

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+}

1290@article{Brady2006a,

1291author = {Brady, E and Hammond, K},

1292file = {: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},