Abstract
This paper explores the recent addition to Agda enabling reflection, in the style of Lisp and Template Haskell. It gives a brief introduction to using reflection, and details the complexities encountered when automating certain proofs with proof by reflection. It presents a library that can be used for automatically quoting a class of concrete Agda terms to a non-dependent, user-defined inductive data type, alleviating some of the burden a programmer faces when using reflection in a practical setting.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
All supporting code, including this paper in Literate Agda format, is available on GitHub. https://github.com/toothbrush/reflection-proofs
- 2.
using the function \(\mathsf {\_\; {\mathop = \limits ^{?}} \text {-}Name\_}\)
- 3.
Of course, having been implemented during a single Agda Implementors’ Meeting [19], the current implementation is more a proof-of-concept, and is still far from being considered finished, so it would be unfair to judge the current implementation all too harshly. In fact, we hope that this work might motivate the Agda developers to include some more features, to make the system truly useful.
References
Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden (2007)
Norell, U.: Dependently typed programming in Agda. In: Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI ’09, pp. 1–2. ACM, New York (2009)
van der Walt, P.: Reflection in Agda. Master’s thesis, Department of Computer Science, Utrecht University, Utrecht, The Netherlands. http://igitur-archive.library.uu.nl/student-theses/2012-1030-200720/UUindex.html (2012)
Pitman, K.M.: Special forms in Lisp. In: Proceedings of the ACM Conference on LISP and Functional Programming, pp. 179–187. ACM (1980)
Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’97 (1997)
Sheard, T., Peyton Jones, S.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, pp. 1–16 (2002)
Martin-Löf, P.: Constructive mathematics and computer programming. In: Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages, pp. 167–184. Prentice-Hall Inc., Upper Saddle River (1985)
Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988)
Oury, N., Swierstra, W.: The power of pi. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP ’08, pp. 39–50. ACM, New York (2008)
Agda Developers: Agda release notes, regarding reflection. The Agda Wiki: http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-8 and http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-3-0 (2013). Accessed 9 Feb 2013
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)
Chlipala, A.: Certified Programming with Dependent Types. MIT Press, New York (2011)
Jedynak, W.: Agda ring solver using reflection. GitHub. https://github.com/wjzz/Agda-reflection-for-semiring-solver (2012). Accessed 26 June 2012
Demers, F., Malenfant, J.: Reflection in logic, functional and object-oriented programming: a short comparative study. In: Proceedings of the IJCAI, vol. 95, pp. 29–38 (1995)
Smith, B.C.: Reflection and semantics in LISP. In: Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’84, pp. 23–35. ACM, New York (1984)
Stump, A.: Directly reflective meta-programming. High. Order Symbolic Comput. 22(2), 115–144 (2009)
Goldberg, A., Robson, D.: Smalltalk-80: The Language and Its Implementation. Addison-Wesley Longman Publishing Co. Inc., Boston (1983)
Sheard, T.: Staged programming. http://web.cecs.pdx.edu/~sheard/staged.html. Accessed 20 Aug 2012
Altenkirch, T.: [Agda mailing list] More powerful quoting and reflection? mailing list communication. https://lists.chalmers.se/pipermail/agda/2012/004127.html (2012). Accessed 14 Sept 2012
Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formalized Reasoning 3(2), 95–152 (2010). (RR-7392 RR-7392)
Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)
Acknowledgements
We would like to thank each of the four anonymous reviewers for taking the time to provide detailed and constructive comments that greatly improved the article.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van der Walt, P., Swierstra, W. (2013). Engineering Proof by Reflection in Agda. In: Hinze, R. (eds) Implementation and Application of Functional Languages. IFL 2012. Lecture Notes in Computer Science(), vol 8241. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41582-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-41582-1_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41581-4
Online ISBN: 978-3-642-41582-1
eBook Packages: Computer ScienceComputer Science (R0)