git.iko.soy/Idris-dev
on master help sign in
More implementation paper
8bf44c2Edwin Brady
impl-paper/library.bib+151−7
compare with master
unifiedsplit
@@ -1,12 +1,24 @@
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−@misc{idristutorial,
4+@inproceedings{pj2006gadts,
5−author = {Brady, Edwin},
5+author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
6+booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
6−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
7+file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
7−title = {{Programming in Idris : a tutorial}},
8+number = {9},
8−url = {http://idris-lang.org/tutorial},
9+pages = {50--61},
10+publisher = {ACM},
11+title = {{Simple unification-based type inference for GADTs}},
12+url = {http://dl.acm.org/citation.cfm?id=1159811},
13+volume = {41},
9−year = {2012}
14+year = {2006}
15+}
16+@book{Hunt,
17+author = {Hunt, Andrew and Thomas, David},
18+booktitle = {Design},
19+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
20+isbn = {020161622X},
21+title = {{The Pragmatic Programmer Chapter 4}}
10}
22}
11@inproceedings{Brady2010,
23@inproceedings{Brady2010,
12author = {Brady, Edwin and Hammond, Kevin},
24author = {Brady, Edwin and Hammond, Kevin},
@@ -124,6 +136,13 @@ url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=
124volume = {43},
136volume = {43},
125year = {2008}
137year = {2008}
126}
138}
139+@book{luo1994,
140+author = {Luo, Z.},
141+publisher = {Oxford University Press, Inc.},
142+title = {{Computation and reasoning: a type theory for computer science}},
143+url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},
144+year = {1994}
145+}
127@article{mccann2000packet,
146@article{mccann2000packet,
128author = {McCann, P.J. and Chandra, S.},
147author = {McCann, P.J. and Chandra, S.},
129journal = {ACM SIGCOMM Computer Communication Review},
148journal = {ACM SIGCOMM Computer Communication Review},
@@ -200,6 +219,19 @@ url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},
200volume = {5520},
219volume = {5520},
201year = {2008}
220year = {2008}
202}
221}
222+@book{While2012,
223+author = {Hunt, Andrew and Thomas, David},
224+booktitle = {Carcinogenesis},
225+doi = {10.1093/carcin/bgs054},
226+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
227+isbn = {020161622X},
228+issn = {1460-2180},
229+number = {3},
230+pmid = {22383472},
231+title = {{The Pragmatic Programmer Chapter 6}},
232+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
233+volume = {33}
234+}
203@inproceedings{madhavapeddy2010turning,
235@inproceedings{madhavapeddy2010turning,
204author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
236author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
205booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
237booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
@@ -312,10 +344,19 @@ url = {http://journals.cambridge.org/abstract_S0956796811000207},
312volume = {21},
344volume = {21},
313year = {2011}
345year = {2011}
314}
346}
347+@inproceedings{pollack1990implicit,
348+author = {Pollack, R.},
349+booktitle = {Informal Proceedings of First Workshop on Logical Frameworks, Antibes},
350+file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Pollack - 1990 - Implicit syntax.pdf:pdf},
351+publisher = {Citeseer},
352+title = {{Implicit syntax}},
353+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
354+year = {1990}
355+}
315@inproceedings{Sculthorpe2009,
356@inproceedings{Sculthorpe2009,
316author = {Sculthorpe, Neil and Nilsson, Henrik},
357author = {Sculthorpe, Neil and Nilsson, Henrik},
317booktitle = {International Conference on Functional Programming ({ICFP} '09)},
358booktitle = {International Conference on Functional Programming ({ICFP} '09)},
318−file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf},
359+file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},
319title = {{Safe functional reactive programming through dependent types}},
360title = {{Safe functional reactive programming through dependent types}},
320url = {http://dl.acm.org/citation.cfm?id=1596558},
361url = {http://dl.acm.org/citation.cfm?id=1596558},
321year = {2009}
362year = {2009}
@@ -357,6 +398,17 @@ title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
357url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
398url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
358year = {2005}
399year = {2005}
359}
400}
401+@article{dybjer1994inductive,
402+author = {Dybjer, P.},
403+journal = {Formal aspects of computing},
404+number = {4},
405+pages = {440--465},
406+publisher = {Springer},
407+title = {{Inductive families}},
408+url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},
409+volume = {6},
410+year = {1994}
411+}
360@article{Hughes1989,
412@article{Hughes1989,
361abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},
413abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},
362author = {Hughes, J},
414author = {Hughes, J},
@@ -414,6 +466,19 @@ title = {{Dependently typed functional programs and their proofs}},
414url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
466url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
415year = {1999}
467year = {1999}
416}
468}
469+@book{The2012,
470+author = {Hunt, Andrew and Thomas, David},
471+booktitle = {Carcinogenesis},
472+doi = {10.1093/carcin/bgs054},
473+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
474+isbn = {020161622X},
475+issn = {1460-2180},
476+number = {3},
477+pmid = {22383472},
478+title = {{The Pragmatic Programmer Chapter 3}},
479+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
480+volume = {33}
481+}
417@inproceedings{oury2008power,
482@inproceedings{oury2008power,
418author = {Oury, N. and Swierstra, W.},
483author = {Oury, N. and Swierstra, W.},
419booktitle = {International Conference on Functional Programming},
484booktitle = {International Conference on Functional Programming},
@@ -591,6 +656,19 @@ url = {http://dl.acm.org/citation.cfm?id=1111039},
591volume = {15},
656volume = {15},
592year = {2010}
657year = {2010}
593}
658}
659+@book{Brady2012,
660+author = {Hunt, Andrew and Thomas, David},
661+booktitle = {Carcinogenesis},
662+doi = {10.1093/carcin/bgs054},
663+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
664+isbn = {020161622X},
665+issn = {1460-2180},
666+number = {3},
667+pmid = {22383472},
668+title = {{The Pragmatic Programmer Chapter 5}},
669+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
670+volume = {33}
671+}
594@inproceedings{Wadler1989,
672@inproceedings{Wadler1989,
595abstract = {From the type of a polymorphic function we can derive a theorem that it satisfies. Every function of the same type satisfies the same theorem. This provides a free source of useful theorems, courtesy of Reynolds' abstraction theorem for the polymorphic lambda calculus.},
673abstract = {From the type of a polymorphic function we can derive a theorem that it satisfies. Every function of the same type satisfies the same theorem. This provides a free source of useful theorems, courtesy of Reynolds' abstraction theorem for the polymorphic lambda calculus.},
596author = {Wadler, Philip},
674author = {Wadler, Philip},
@@ -625,6 +703,19 @@ title = {{The implicit calculus of constructions as a programming language with
625url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
703url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
626year = {2008}
704year = {2008}
627}
705}
706+@book{Philosophy2012,
707+author = {Hunt, Andrew and Thomas, David},
708+booktitle = {Carcinogenesis},
709+doi = {10.1093/carcin/bgs054},
710+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
711+isbn = {020161622X},
712+issn = {1460-2180},
713+number = {3},
714+pmid = {22383472},
715+title = {{The Pragmatic Programmer Chapter 1}},
716+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
717+volume = {33}
718+}
628@article{landin1966next,
719@article{landin1966next,
629author = {Landin, P.J.},
720author = {Landin, P.J.},
630file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
721file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
@@ -646,6 +737,19 @@ issn = {1478-6729},
646pmid = {22215642},
737pmid = {22215642},
647title = {{The Design of Design Chapter 2}}
738title = {{The Design of Design Chapter 2}}
648}
739}
740+@book{Approach2012,
741+author = {Hunt, Andrew and Thomas, David},
742+booktitle = {Carcinogenesis},
743+doi = {10.1093/carcin/bgs054},
744+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
745+isbn = {020161622X},
746+issn = {1460-2180},
747+number = {3},
748+pmid = {22383472},
749+title = {{The Pragmatic Programmer Chapter 2}},
750+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
751+volume = {33}
752+}
649@inproceedings{Brady2003,
753@inproceedings{Brady2003,
650author = {Brady, Edwin and McBride, Conor and McKinna, James},
754author = {Brady, Edwin and McBride, Conor and McKinna, James},
651booktitle = {Types for Proofs and Programs},
755booktitle = {Types for Proofs and Programs},
@@ -665,6 +769,13 @@ issn = {1478-6729},
665pmid = {22215642},
769pmid = {22215642},
666title = {{The Design of Design Chapter 3}}
770title = {{The Design of Design Chapter 3}}
667}
771}
772+@book{Fowler,
773+author = {Fowler, Martin},
774+booktitle = {Language},
775+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
776+isbn = {9780132107549},
777+title = {{Domain Specific Languages Chapter 2}}
778+}
668@article{Abel2010,
779@article{Abel2010,
669abstract = {Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.},
780abstract = {Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.},
670author = {Abel, Andreas},
781author = {Abel, Andreas},
@@ -766,6 +877,13 @@ title = {{Idris --- Systems Programming Meets Full Dependent Types}},
766url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
877url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
767year = {2011}
878year = {2011}
768}
879}
880+@misc{idristutorial,
881+author = {Brady, Edwin},
882+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
883+title = {{Programming in Idris : a tutorial}},
884+url = {http://idris-lang.org/tutorial},
885+year = {2012}
886+}
769@article{Steiner1988,
887@article{Steiner1988,
770author = {Steiner, JG},
888author = {Steiner, JG},
771file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
889file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
@@ -782,6 +900,19 @@ title = {{Cryptographic verification by typing for a sample protocol implementat
782url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
900url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
783year = {2010}
901year = {2010}
784}
902}
903+@book{An2012,
904+author = {Fowler, Martin},
905+booktitle = {Carcinogenesis},
906+doi = {10.1093/carcin/bgs054},
907+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
908+isbn = {9780132107549},
909+issn = {1460-2180},
910+number = {3},
911+pmid = {22383472},
912+title = {{Domain Specific Languages Chapter 1}},
913+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
914+volume = {33}
915+}
785@inproceedings{augustsson2008paradise,
916@inproceedings{augustsson2008paradise,
786author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
917author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
787booktitle = {International Conference on Functional Programming},
918booktitle = {International Conference on Functional Programming},
@@ -1023,6 +1154,19 @@ pmid = {22215642},
1023title = {{Security Engineering Chapter 18}},
1154title = {{Security Engineering Chapter 18}},
1024volume = {34}
1155volume = {34}
1025}
1156}
1157+@book{Choosing2012,
1158+author = {Fowler, Martin},
1159+booktitle = {Carcinogenesis},
1160+doi = {10.1093/carcin/bgs054},
1161+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
1162+isbn = {9780132107549},
1163+issn = {1460-2180},
1164+number = {3},
1165+pmid = {22383472},
1166+title = {{Domain Specific Languages Chapter 6}},
1167+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
1168+volume = {33}
1169+}
1026@article{Xi1998,
1170@article{Xi1998,
1027abstract = {We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and effectiveness of our approach.},
1171abstract = {We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and effectiveness of our approach.},
1028author = {Xi, Hongwei and Pfenning, Frank},
1172author = {Xi, Hongwei and Pfenning, Frank},
impl-paper/library.ltx+4−4
@@ -141,9 +141,9 @@
141%%% Nat
141%%% Nat
142
142
143\newcommand{\NatPackage}{
143\newcommand{\NatPackage}{
144− \newcommand{\Nat}{\TC{\mathbb{N}}}
144+ \newcommand{\Nat}{\TC{Nat}}
145− \newcommand{\Z}{\DC{0}}
145+ \newcommand{\Z}{\DC{O}}
146− \newcommand{\suc}{\DC{s}}
146+ \newcommand{\suc}{\DC{S}}
147 \newcommand{\NatDecl}{
147 \newcommand{\NatDecl}{
148 \Data \hg
148 \Data \hg
149 \Axiom{\Nat\Hab\Type} \hg
149 \Axiom{\Nat\Hab\Type} \hg
@@ -246,7 +246,7 @@
246
246
247\newcommand{\VectPackage}{
247\newcommand{\VectPackage}{
248 \newcommand{\Vect}{\TC{Vect}}
248 \newcommand{\Vect}{\TC{Vect}}
249− \newcommand{\vnil}{\varepsilon}
249+ \newcommand{\vnil}{\DC{Nil}}
250 \newcommand{\vcons}{\,\dcolon\,}
250 \newcommand{\vcons}{\,\dcolon\,}
251 \newcommand{\vsnoc}{\,\dcolon\,}
251 \newcommand{\vsnoc}{\,\dcolon\,}
252 \newcommand{\VectConsDecl}{
252 \newcommand{\VectConsDecl}{
impl-paper/macros.ltx+8−6
@@ -108,10 +108,10 @@
108
108
109%%%%%%%%%%%% FONTS
109%%%%%%%%%%%% FONTS
110
110
111−\newcommand{\TC}[1]{\mathsf{#1}}
111+\newcommand{\TC}[1]{\mathtt{#1}}
112−\newcommand{\DC}[1]{\mathsf{#1}}
112+\newcommand{\DC}[1]{\mathtt{#1}}
113\newcommand{\VV}[1]{\mathit{#1}}
113\newcommand{\VV}[1]{\mathit{#1}}
114−\newcommand{\FN}[1]{\mathbf{#1}}
114+\newcommand{\FN}[1]{\mathtt{#1}}
115\newcommand{\HFN}[1]{\mathtt{#1}}
115\newcommand{\HFN}[1]{\mathtt{#1}}
116\newcommand{\RW}[1]{\underline{\textrm{#1}}}
116\newcommand{\RW}[1]{\underline{\textrm{#1}}}
117\newcommand{\MO}[1]{\mbox{\textsc{#1}}}
117\newcommand{\MO}[1]{\mbox{\textsc{#1}}}
@@ -405,6 +405,8 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
405\newcommand{\lam}[2]{\lambda#1\pad{\!}{:}#2}
405\newcommand{\lam}[2]{\lambda#1\pad{\!}{:}#2}
406\newcommand{\fbind}[3]{(#1\Hab#2)\to#3}
406\newcommand{\fbind}[3]{(#1\Hab#2)\to#3}
407\newcommand{\all}[2]{\forall#1\pad{\!}{:}#2}
407\newcommand{\all}[2]{\forall#1\pad{\!}{:}#2}
408+\newcommand{\pat}[2]{\RW{pat}\:#1\pad{\!}{:}#2}
409+\newcommand{\pty}[2]{\RW{pty}\:#1\pad{\!}{:}#2}
408\newcommand{\hole}[2]{?#1\pad{\!}{:}#2}
410\newcommand{\hole}[2]{?#1\pad{\!}{:}#2}
409\newcommand{\guess}[3]{?#1\pad{\!}{:}#2\approx#3}
411\newcommand{\guess}[3]{?#1\pad{\!}{:}#2\approx#3}
410\newcommand{\remlam}[2]{\lambda\{#1\pad{\!}{:}#2\}}
412\newcommand{\remlam}[2]{\lambda\{#1\pad{\!}{:}#2\}}
@@ -561,8 +563,8 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
561\newcommand{\CoqType}{\TC{Type}}
563\newcommand{\CoqType}{\TC{Type}}
562
564
563\newcommand{\List}{\TC{List}}
565\newcommand{\List}{\TC{List}}
564−\newcommand{\nil}{\DC{nil}}
566+\newcommand{\nil}{\DC{Nil}}
565−\newcommand{\cons}{\DC{cons}}
567+\newcommand{\cons}{\DC{::}}
566
568
567\newcommand{\Zip}{\TC{Tsil}}
569\newcommand{\Zip}{\TC{Tsil}}
568\newcommand{\zip}{\FN{tsil}}
570\newcommand{\zip}{\FN{tsil}}
@@ -627,7 +629,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
627
629
628% Reductions
630% Reductions
629
631
630−\newcommand{\reduces}{\mapsto}
632+\newcommand{\reduces}{\rhd}
631\newcommand{\translation}{\Rightarrow}
633\newcommand{\translation}{\Rightarrow}
632%\newcommand{\reducesn}[1]{\reduces\hspace*{-0.15cm}_{#1}}
634%\newcommand{\reducesn}[1]{\reduces\hspace*{-0.15cm}_{#1}}
633%\newcommand{\reducesto}{\reduces\hspace*{-0.15cm}^{*}}
635%\newcommand{\reducesto}{\reduces\hspace*{-0.15cm}^{*}}
impl-paper/typechecking.tex+228−10
@@ -1,21 +1,37 @@
1\section{The Core Type Theory}
1\section{The Core Type Theory}
2
2
3High level \Idris{} programs, as described in Section \ref{sect:hll} are
3High level \Idris{} programs, as described in Section \ref{sect:hll} are
4−\remph{elaborated} to a small core language, \TT{}, then type checked. We keep the
4+\remph{elaborated} to a small core language, \TT{}, then type checked.
5+\TT{} is a dependently typed $\lambda$-calculus with inductive families
6+and pattern matching definitions similar to UTT~\cite{luo1994}, and building
7+on an earlier implementation, \Ivor{}~\cite{Brady2006b}.
8+We keep the
5−core language as small as is reasonable. This has several advantages: it is
9+core language as small as is reasonable, which has several advantages: it is
6easy to type check, since type checking dependent type theory is well understood
10easy to type check, since type checking dependent type theory is well understood
7~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping
11~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping
8−the language small increases our confidence that these important components of
12+the core language small increases our confidence that these important components of
9the language are correct. In this section, we describe \TT{} and
13the language are correct. In this section, we describe \TT{} and
10its semantics.
14its semantics.
11
15
12\subsection{\TT{} syntax}
16\subsection{\TT{} syntax}
13
17
14−The syntax of \TT{} expressions is given in Figure \ref{ttsyn}.
18+The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:
19+
20+\begin{itemize}
21+\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.
22+\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.
23+\item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the
24+type of types.
25+\end{itemize}
26+
27+We may also write the function space $\all{\vx}{\vS}\SC\vT$ as $(\vx\Hab\vS)\to\vT$,
28+or $\vS\to\vT$ if $\vx$ is not free in $\vT$, to make the notation more consistent with
29+the high level language. Universe levels on sets ($\Type_i$) may be left implicit and
30+inferred by the machine~\cite{pollack1990implicit}.
15
31
16\FFIG{
32\FFIG{
17−\begin{array}{rll@{\hg}|rll}
33+\begin{array}{rll@{\hg}rll}
18−\vt ::= & \Type_i & (\mbox{type universes}) &
34+\vt ::= & \vc & (\mbox{constants}) &
19\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\
35\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\
20
36
21 \mid & \vx & (\mbox{variable}) &
37 \mid & \vx & (\mbox{variable}) &
@@ -24,16 +40,218 @@ The syntax of \TT{} expressions is given in Figure \ref{ttsyn}.
24 \mid & \vb\SC\:\vt & (\mbox{binding}) &
40 \mid & \vb\SC\:\vt & (\mbox{binding}) &
25 \mid & \all{\vx}{\vt} & (\mbox{function space}) \\
41 \mid & \all{\vx}{\vt} & (\mbox{function space}) \\
26
42
27− \mid & \vt\:\vt & (\mbox{application})
43+ \mid & \vt\:\vt & (\mbox{application}) &
28−
44+% \mid & \pat{\vx}{\vt} & (\mbox{pattern variable}) \\
45+% & & &
46+% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\
47+\medskip\\
48+ \vc ::= & \Type_i & (\mbox{type universes}) \\
49+ \mid & \vi & (\mbox{integer literal}) \\
50+ \mid & \VV{str} & (\mbox{string literal}) \\
29\end{array}
51\end{array}
30}
52}
31{\TT{} expression syntax}
53{\TT{} expression syntax}
32{ttsyn}
54{ttsyn}
33
55
34−\subsection{Evaluation rules}
56+\subsection{\TT{} semantics}
57+
58+The static and dynamic semantics of \TT{} are defined mutually, since
59+evaluation relies on a well-typed term, and type checking relies on
60+evaluation. Everything is defined relative
61+to a context, $\Gamma$. The empty context
62+is valid, as is a context extended with a $\lambda$, $\forall$ or
63+$\LET$ binding:
64+
65+\DM{
66+\Axiom{\proves\RW{valid}}
67+\hg
68+\Rule{\Gamma\proves\RW{valid}}
69+{\Gamma;\vb\proves\RW{valid}}
70+}
71+
72+\subsubsection{Evaluation}
73+
74+Conceptually, evaluation of \TT{} is defined by contraction schemes, given in Figure
75+\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
76+by one of the following schemes:
77+
78+\begin{itemize}
79+\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for
80+the bound variable. We define $\beta$-constraction simply by replacing the $\lambda$-binding
81+with a $\LET$ binding.
82+\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.
83+\end{itemize}
84+
85+\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation
86+is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)
87+is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
88+then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
89+contractions and reversed contractions. Terms which are convertible are also said to
90+be computationally equal.
91+
92+\FFIG{
93+\begin{array}{lc}
94+\beta\mathrm{-contraction} &
95+\Axiom{
96+\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\:\vs\leadsto\LET\:\vx\defq\vs\Hab\vS\SC\vt
97+} \\
98+\delta\mathrm{-contraction} &
99+\Axiom{
100+\Gamma;\LET\:\vx\defq\vs\Hab\vS;\Gamma'
101+\proves
102+\vx\leadsto\vs
103+}
104+\end{array}
105+}
106+{\TT{} contraction schemes}
107+{ttcontract}
108+
109+\subsubsection{Cumulativity}
110+
111+Figure \ref{cumul} gives the \demph{cumulativity} relation.
112+
113+\FFIG{
114+\begin{array}{c}
115+\Rule{\Gamma\proves\vS\converts\vT}
116+{\Gamma\proves\vS\cumul\vT}
117+\hg
118+\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
119+\\
120+\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
121+{\Gamma\proves\vR\cumul\vT}
122+\\
123+\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}
124+{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}
125+\end{array}
126+}
127+{Cumulativity}
128+{cumul}
129+
130+\subsubsection{Typing rules}
131+
132+\FFIG{\begin{array}{c}
133+\mathsf{Type}\:
134+\Rule{\Gamma\proves\RW{valid}}
135+{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
136+\\
137+\mathsf{Var}_1\:
138+\Rule{(\lam{\vx}{\vS})\in\Gamma}
139+{\Gamma\vdash\vx\Hab\vS}
140+\hg
141+\mathsf{Var}_2\:
142+\Rule{(\all{\vx}{\vS})\in\Gamma}
143+{\Gamma\vdash\vx\Hab\vS}
144+\hg
145+\mathsf{Val}\:
146+\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
147+{\Gamma\vdash\vx\Hab\vS}
148+\\
149+%\mathsf{Pat}_1\:
150+%\Rule{(\pat{\vx}{\vS})\in\Gamma}
151+%{\Gamma\vdash\vx\Hab\vS}
152+%\hg
153+%\mathsf{Pat}_2\:
154+%\Rule{(\pty{\vx}{\vS})\in\Gamma}
155+%{\Gamma\vdash\vx\Hab\vS}
156+\\
157+\mathsf{App}\:
158+\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
159+{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}
160+\\
161+\mathsf{Lam}\:
162+\Rule{\Gamma;\lam{\vx}{\vS}\vdash\ve\Hab\vT\hg\Gamma\proves\fbind{\vx}{\vS}{\vT}\Hab\Type_n}
163+{\Gamma\vdash\lam{\vx}{\vS}.\ve\Hab\fbind{\vx}{\vS}{\vT}}
164+\\
165+\mathsf{Forall}\:
166+\Rule{\Gamma;\all{\vx}{\vS}\vdash\vT\Hab\Type_m\hg\Gamma\vdash\vS\Hab\Type_n}
167+{\Gamma\vdash\fbind{\vx}{\vS}{\vT}\Hab\Type_p}
168+\:(\exists\vp.\vm\le\vp,\:\vn\le\vp)
169+\\
170+\mathsf{Let}\:
171+\Rule{\begin{array}{c}\Gamma\proves\ve_1\Hab\vS\hg
172+ \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\ve_2\Hab\vT\\
173+ \Gamma\proves\vS\Hab\Type_n\hg
174+ \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\vT\Hab\Type_n\end{array}
175+ }
176+{\Gamma\vdash\LET\:\vx\defq\ve_1\Hab\vS\SC\:\ve_2\Hab
177+ \vT[\ve_1/\vx]}
178+%\Let\:\vx\Hab\vS\defq\ve_1\:\IN\:\vT}
179+\\
180+
181+\mathsf{Conv}\:
182+\Rule{\Gamma\proves\vx\Hab\vA\hg\Gamma\proves\vA'\Hab\Type_n\hg
183+ \Gamma\proves\vA\cumul\vA'}
184+ {\Gamma\proves\vx\Hab\vA'}
185+\end{array}
186+}
187+{Typing rules for \TT{}}
188+{typerules}
189+
190+\subsection{Inductive Families}
191+
192+Inductive families \cite{dybjer1994inductive} are a form of simultaneously
193+defined collection of algebraic data types (such as Haskell
194+\texttt{data} declarations) which can be parametrised over
195+\remph{values} as well as types. An inductive family is declared
196+in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
197+as
198+follows, using the de Bruijn telescope notation, $\tx$, to indicate a
199+sequence of zero or more $\vx$:
200+
201+\DM{
202+\AR{
203+\Data\hg\TC{T}\:(\tx\Hab\ttt)\Hab\vt\hg\Where\hg
204+\DC{c}_1\Hab\vt\:\mid\:\ldots\:\mid\:\DC{c}_n\Hab\vt
205+}
206+}
207+
208+Constructors may take recursive arguments in the family
209+$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---
210+if such indices do not involve $\TC{T}$ then the constructor is
211+\demph{strictly positive}, which ensures that recursive arguments of the
212+constructor are structurally smaller than the value itself.
213+
214+For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
215+
216+\DM{
217+\Data\hg\Nat\Hab\Type\hg\Where\hg\Z\Hab\Nat\:\mid\:\suc\Hab\fbind{\vk}{\Nat}{\Nat}
218+}
219+
220+A data type may have zero or more parameters (which are invariant
221+across a structure) and a number of indices, given by the type. For
222+example, the \TT{} equivalent of \tTC{List} is parametrised over its element type:
223+
224+\DM{
225+\AR{
226+\Data\hg\List\:(\va\Hab\Type)\Hab\Type\hg\Where
227+\ARd{
228+& \nil\Hab\List\:\va\\
229+\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\:\va}{\List\:\va}}
230+}
231+}
232+}
233+
234+Types can be
235+parametrised over values. Using this, we can declare the type of
236+vectors (lists with length), where the empty list is statically known
237+to have length zero, and the non empty list is statically known to
238+have a non zero length. The \TT{} equivalent of \tTC{Vect} is parametrised over its element type,
239+like $\List$, but \remph{indexed} over its length. Note also that the length
240+index $\vk$ is given \remph{explicitly}.
241+
242+\DM{
243+\AR{
244+\Data\hg\Vect\:(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\
245+\hg\hg\ARd{
246+& \nil\Hab\Vect\:\va\:\Z\\
247+\mid & (\cons)\Hab\fbind{\vk}{\Nat}{
248+\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\:\va\:\vk}{\Vect\:\va\:(\suc\:\vk)}}
249+}
250+}
251+}
252+}
35
253
36−\subsection{Typing rules}
254+\subsection{Pattern matching definitions}
37
255
38\subsection{The Development Calculus \TTdev}
256\subsection{The Development Calculus \TTdev}
39
257