Jesper Cockx
Abstract
In a dependently typed language, we can guarantee correctness of our programs by providing formal proofs. To check them, the typechecker elaborates these programs and proofs into a low level core language. However, this core language is by nature hard to understand by mere humans, so how can we know we proved the right thing? This question occurs in particular for dependent copattern matching, a powerful language construct for writing programs and proofs by dependent case analysis and mixed induction/coinduction. A definition by copattern matching consists of a list of clauses that are elaborated to a case tree, which can be further translated to primitive eliminators. In previous work this second step has received a lot of attention, but the first step has been mostly ignored so far.
We present an algorithm elaborating definitions by dependent copattern matching to a core language with inductive datatypes, coinductive record types, an identity type, and constants defined by well-typed case trees. To ensure correctness, we prove that elaboration preserves the first-match semantics of the user clauses. Based on this theoretical work, we reimplement the algorithm used by Agda to check left-hand sides of definitions by pattern matching. The new implementation is at the same time more general and less complex, and fixes a number of bugs and usability issues with the old version. Thus we take another step towards the formally verified implementation of a practical dependently typed language.
Supplemental Material
- Andreas Abel and Brigitte Pientka. 2013. Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity. In Proceedings of the Eighteenth ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA, September 25-27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM Press, 185–196. Google Scholar
Digital Library
- Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming Infinite Structures by Observations. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’13, Rome, Italy, January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM Press, 27–38. http://dl.acm.org/ citation.cfm?id=2429069 Google ScholarDigital Library
- Agda development team. 2017. Agda 2.5.3 documentation. http://agda.readthedocs.io/en/v2.5.3/Google Scholar
- Agda issue. 2017a. Disambiguation of type based on pattern leads to non-unique meta solution. (2017). https://github. com/agda/agda/issues/2834 (on the Agda bug tracker).Google Scholar
- Agda issue. 2017b. Internal error in src/full/Agda/TypeChecking/Coverage/Match.hs:312. (2017). https://github.com/agda/ agda/issues/2874 (on the Agda bug tracker).Google Scholar
- Agda issue. 2017c. Panic: unbound variable. (2017). https://github.com/agda/agda/issues/2856 (on the Agda bug tracker).Google Scholar
- Agda issue. 2017d. Record constructor is accepted, record pattern is not. (2017). https://github.com/agda/agda/issues/2850 (on the Agda bug tracker).Google Scholar
- Agda issue. 2018a. Mismatch between order of matching in clauses and case tree; subject reduction broken. (2018). https: //github.com/agda/agda/issues/2964 (on the Agda bug tracker).Google Scholar
- Agda issue. 2018b. Unifier throws away pattern. (2018). https://github.com/agda/agda/issues/2896 (on the Agda bug tracker).Google Scholar
- Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation 2, 3 (1992), 297–347.Google ScholarCross Ref
- Lennart Augustsson. 1985. Compiling Pattern Matching. In Functional Programming Languages and Computer Architecture, FPCA 1985, Nancy, France, September 16-19, 1985, Proceedings (Lecture Notes in Computer Science), Jean-Pierre Jouannaud (Ed.), Vol. 201. Springer, 368–381. Google ScholarDigital Library
- Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. 2017. Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer, 111–140. Google ScholarDigital Library
- Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.Google ScholarCross Ref
- Edwin Brady, Conor McBride, and James McKinna. 2003. Inductive Families Need Not Store Their Indices. In Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers (Lecture Notes in Computer Science), Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.), Vol. 3085. Springer, 115–129.Google Scholar
- Luca Cardelli. 1984. Compiling a Functional Language. In Proceedings of the 1984 ACM Conference on LISP and Functional Programming, August 5-8, 1984, Austin, Texas, USA. ACM Press, 208–217. http://lucacardelli.name/Papers/CompilingML. A4.pdf Google ScholarDigital Library
- Jesper Cockx. 2017. Dependent pattern matching and proof-relevant unification. Ph.D. Dissertation. KU Leuven.Google Scholar
- Jesper Cockx, Dominique Devriese, and Frank Piessens. 2016. Unifiers as equivalences: proof-relevant unification of dependently typed data, See { Garrigue et al. 2016 }, 270–283. Google ScholarDigital Library
- Thierry Coquand. 1992. Pattern Matching with Dependent Types. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden, June 1992, Bengt Nordström, Kent Pettersson, and Gordon Plotkin (Eds.). 71–83. http: //www.cse.chalmers.se/~coquand/pattern.psGoogle Scholar
- Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings (Lecture Notes in Computer Science), Amy P. Felty and Aart Middeldorp (Eds.), Vol. 9195. Springer, 378–388.Google ScholarCross Ref
- Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). 2016. Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. ACM Press. Google ScholarDigital Library
- Healfdene Goguen, Conor McBride, and James McKinna. 2006. Eliminating Dependent Pattern Matching. In Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday (Lecture Notes in Computer Science), Kokichi Futatsugi, Jean-Pierre Jouannaud, and José Meseguer (Eds.), Vol. 4060. Springer, 521–540.Google Scholar
- INRIA. 2017. The Coq Proof Assistant Reference Manual (version 8.7 ed.). INRIA. http://coq.inria.fr/Google Scholar
- Neelakantan R. Krishnaswami. 2009. Focusing on pattern matching. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM Press, 366–378. Google ScholarDigital Library
- Daniel R. Licata, Noam Zeilberger, and Robert Harper. 2008. Focusing on Binding and Computation. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, Frank Pfenning (Ed.). IEEE Computer Society Press, 241–252. Google ScholarDigital Library
- Luc Maranget. 1992. Compiling Lazy Pattern Matching. In LISP and Functional Programming. 21–31. Google ScholarDigital Library
- Conor McBride. 2000. Dependently typed functional programs and their proofs. Ph.D. Dissertation. University of Edinburgh.Google Scholar
- Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers University of Technology.Google Scholar
- Nicolas Oury. 2007. Pattern matching coverage checking with dependent types using set approximations. In Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007, Aaron Stump and Hongwei Xi (Eds.). ACM Press, 47–56. Google ScholarDigital Library
- Robert Pollack. 1998. How to Believe a Machine-Checked Proof. In Twenty Five Years of Constructive Type Theory, Giovanni Sambin and Jan Smith (Eds.). Oxford University Press. http://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdfGoogle Scholar
- Anton Setzer, Andreas Abel, Brigitte Pientka, and David Thibodeau. 2014. Unnesting of Copatterns. In Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (Lecture Notes in Computer Science), Gilles Dowek (Ed.), Vol. 8560. Springer, 31–45.Google ScholarCross Ref
- Matthieu Sozeau. 2010. Equations: A Dependent Pattern-Matching Compiler. In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Lecture Notes in Computer Science), Matt Kaufmann and Lawrence C. Paulson (Eds.), Vol. 6172. Springer, 419–434. Google ScholarDigital Library
- David Thibodeau, Andrew Cave, and Brigitte Pientka. 2016. Indexed codata types, See { Garrigue et al. 2016 }, 351–363. Google ScholarDigital Library
- Noam Zeilberger. 2008. Focusing and higher-order abstract syntax. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, George C. Necula and Philip Wadler (Eds.). ACM Press, 359–369. Google ScholarDigital Library
- Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph.D. Dissertation. Carnegie Mellon University. http://software.imdea.org/~noam.zeilberger/thesis.pdf Google ScholarDigital Library
Index Terms
- Elaborating dependent (co)pattern matching
Recommendations
Pattern matching without K
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programmingDependent pattern matching is an intuitive way to write programs and proofs in dependently typed languages. It is reminiscent of both pattern matching in functional languages and case analysis in on-paper mathematics. However, in general it is ...
Pattern matching without K
ICFP '14Dependent pattern matching is an intuitive way to write programs and proofs in dependently typed languages. It is reminiscent of both pattern matching in functional languages and case analysis in on-paper mathematics. However, in general it is ...
Decidability of conversion for type theory in type theory
Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other ...
Comments