Eliminating dependent pattern matching without K. (English) Zbl 1419.68037
Summary: Dependent 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 incompatible with new type theories such as homotopy type theory (HoTT). As a consequence, proofs in such theories are typically harder to write and to understand. The source of this incompatibility is the reliance of dependent pattern matching on the so-called K axiom – also known as the uniqueness of identity proofs – which is inadmissible in HoTT. In this paper, we propose a new criterion for dependent pattern matching without K, and prove it correct by a translation to eliminators in the style of H. Goguen et al. [Lect. Notes Comput. Sci. 4060, 521–540 (2006; Zbl 1132.68327)]. Our criterion is both less restrictive than existing proposals, and solves a previously undetected problem in the old criterion offered by Agda. It has been implemented in Agda and is the first to be supported by a formal proof. Thus, it brings the benefits of dependent pattern matching to contexts where we cannot assume K, such as HoTT.
MSC:
| 68N18 | Functional programming and lambda calculus |
| 03B15 | Higher-order logic; type theory (MSC2010) |
| 03G30 | Categorical logic, topoi |
| 55U40 | Topological categories, foundations of homotopy theory |
Citations:
Zbl 1132.68327References:
| [1] | AltenkirchT. (2012) Without-K problem. Available at: https://lists.chalmers.se/pipermail/agda/2012/004104.html. On the Agda mailing list. (last accessed date 09/08/2016) |
| [2] | AugustssonL. (1985) Compiling pattern matching. In Functional Programming Languages and Computer Architecture: Nancy, France, September 16-19, 1985, JouannaudJ.-P. (ed), Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 368-381. |
| [3] | BarrasB., CorbineauP., GrégoireB., HerbelinH. & SacchiniJ. L. (2009) A new elimination rule for the calculus of inductive constructions. In Types for Proofs and Programs: International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 32-48. · Zbl 1246.68085 |
| [4] | BezemM., CoquandT. & HuberS. (2014) A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), MatthesR. and SchubertA. (eds), Leibniz International Proceedings in Informatics (LIPIcs), vol. 26. Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 107-128. · Zbl 1359.03009 |
| [5] | BoutillierP. (2014) De nouveaux outils pour Calculer avec des inductifs en Coq. PhD Thesis, Université Paris-Diderot-Paris VII. |
| [6] | BradyE. (2013) Idris, a general purpose dependently typed programming language: Design and implementation. J. Funct. Program.23(5), 552-593.10.1017/S095679681300018X · Zbl 1295.68059 · doi:10.1017/S095679681300018X |
| [7] | CockxJ. (2014) Yet another way Agda –without-K is incompatible with univalence. Available at: https://lists.chalmers.se/pipermail/agda/2014/006367.html. On the Agda mailing list. (last accessed date 09/08/2016) |
| [8] | CockxJ., DevrieseD. & PiessensF. (2014) Pattern matching without K. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA: ACM, pp. 257-268. · Zbl 1345.68045 |
| [9] | CockxJ., DevrieseD. & PiessensF. (to appear) Unifiers as Equivalences: Proof-relevant unification of dependently typed data. In Proceedings of the 21th ACM SIGPLAN International Conference on Functional Programming. ACM. · Zbl 1360.68321 |
| [10] | CohenC., CoquandT., HuberS. & MörtbergA. (2015) Cubical type theory: A constructive interpretation of the univalence axiom. http://www.cse.chalmers.se/ coquand/cubicaltt.pdf (last accessed date 09/08/2016) |
| [11] | CoquandT. (1992) Pattern matching with dependent types. In Proceedings of the 3rd Workshop on Types for Proofs and Program, pp. 66-79. |
| [12] | DagandP.-E. (2013) A Cosmology of Datatypes: Reusability and Dependent Types. PhD Thesis, University of Strathclyde. |
| [13] | DanielssonN.-A. (2013) Experiments related to equality. Available at: http://www.cse.chalmers.se/ nad/repos/equality/. Agda code. (last accessed date 09/08/2016) |
| [14] | de MouraL., KongS., AvigadJ., van DoornF. & von RaumerJ. (2015) The lean theorem prover (system description). In Proceedings of 25th International Conference on Automated Deduction (CADE-25), FeltyP. Amy and MiddeldorpA. (eds). Cham: Springer International Publishing, pp. 378-388. · Zbl 1465.68279 |
| [15] | DevrieseD. & PiessensF. (2011) On the bright side of type classes: Instance arguments in Agda. In ACM SIGPLAN International Conference on Functional Programming (ICFP), New York, NY, USA: ACM, pp. 143-155. · Zbl 1323.68108 |
| [16] | DybjerP. (1991) Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In Proceedings of the 1st Workshop on Logical Frameworks, HuetG. and PlotkinG. (eds) pp. 213-230. |
| [17] | GoguenH., McBrideC. & McKinnaJ. (2006) Eliminating dependent pattern matching. In Algebra, Meaning, and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 521-540.2281326 · Zbl 1132.68327 |
| [18] | HofmannM. & StreicherT. (1994) The groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 208-212. |
| [19] | JouannaudJ.-P. & KirchnerC. (1990) Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification In Computational Logic: Essays in Honor of Alan Robinson, LassezJ. L. (ed). |
| [20] | KrausN., EscardóM., CoquandT. & AltenkirchT. (2013) Generalizations of Hedberg’s theorem. In Typed Lambda Calculi and Applications, HasegawaM. (ed). Springer, pp. 173-188. · Zbl 1433.03032 |
| [21] | KrausN. & SattlerC. (2015) On the hierarchy of univalent universes: U(n) is not n-truncated. ACM Trans. Comput. Logic.16(2), 18:1-18:12. New York, NY, USA: ACM. · Zbl 1354.03100 |
| [22] | LicataD. (2011) Just kidding: Understanding identity elimination in homotopy type theory. Available at: http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/. (last accessed date 09/08/2016) |
| [23] | LicataD. R. & ShulmanM. (2013) Calculating the fundamental group of the circle in homotopy type theory. In Proceedings of 28th Annual IEEE/ACM Symposium on Logic in Computer Science. · Zbl 1369.03097 |
| [24] | LuoZ. (1994) Computation and Reasoning: A Type Theory for Computer Science, International Series of Monographs on Computer Science, vol. 11. · Zbl 0823.68101 |
| [25] | ManginC. & SozeauM. (2015) Equations for hereditary substitution in Leivant’s predicative system F: A case study. In Proceedings of the 10th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, CervesatoI. and ChaudhuriK. pp. 71-86. |
| [26] | MarangetL. (2008) Compiling pattern matching to good decision trees. In Proceedings of the 2008 ACM SIGPLAN Workshop on ML. New York, NY, USA: ACM, pp. 35-46. |
| [27] | Martin-LöfP. (1984) Intuitionistic Type Theory. Naples: Bibliopolis Number 1 in Studies in Proof Theory, vol. 76. |
| [28] | McBrideC. (1998) Towards dependent pattern matching in LEGO. TYPES meeting. |
| [29] | McBrideC. (2000) Dependently Typed Functional Programs and their Proofs. PhD Thesis, University of Edinburgh. |
| [30] | McBrideC. (2002) Elimination with a motive. In Types for Proofs and Programs: International Workshop, TYPES 2000 Durham, UK, December 8-12, 2000 Selected Papers, CallaghanP., LuoZ., McKinnaJ., and PollackR. (eds). Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 197-216. · Zbl 1054.03501 |
| [31] | McBrideC. (2005) Epigram: Practical programming with dependent types. In Advanced Functional ProgrammingVeneV. and UustaluT. (eds). Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 130-170. · Zbl 1158.68356 |
| [32] | McBrideC. & McKinnaJ. (2004) The view from the left. J. Funct. Program.14(1), 69-111.10.1017/S09567968030048292055218 · Zbl 1069.68539 · doi:10.1017/S0956796803004829 |
| [33] | McBrideC., GoguenH. & McKinnaJ. (2006) A few constructions on constructors. In Types for Proofs and Programs, FilliâtreJ.-C., Paulin-MohringC., and WernerB. (eds). Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 186-200. · Zbl 1172.68548 |
| [34] | NorellU. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Chalmers University of Technology. |
| [35] | NorellU., AbelA. & DanielssonN. A. (2012) Release notes for Agda 2 version 2.3.2. Available at: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-3-2. (last accessed date 09/08/2016) |
| [36] | Paulin-MohringC. (1993) Inductive definitions in the System Coq - rules and properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA ’93. London, UK: Springer-Verlag, pp. 328-345. · Zbl 0844.68073 |
| [37] | ReedJ. (2013) Another possible without-K problem. Available at: https://lists.chalmers.se/pipermail/agda/2013/005578.html. On the Agda mailing list. (last accessed date 09/08/2016) |
| [38] | Sicard-RamírezA. (2013) -without-K option too restrictive?. Available at: https://lists.chalmers.se/pipermail/agda/2013/005407.html. On the Agda mailing list. (last accessed date 09/08/2016) |
| [39] | SozeauM. (2010) Equations: A dependent pattern-matching compiler. In Interactive Theorem Proving, KaufmannM. and PaulsonL. C. (eds). Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 419-434. · Zbl 1291.68369 |
| [40] | SozeauM. (2015) Coq support for HoTT. In Workshop on Homotopy Type Theory / Univalent Foundations. |
| [41] | The Coq development team. (2012) The Coq Proof Assistant Reference Manual. LogiCal Project. Available at: http://coq.inria.fr. Version 8.4. |
| [42] | The Univalent Foundations Program. (2013) Homotopy Type Theory: Univalent Foundations of Mathematics. Available at: http://homotopytypetheory.org/book, Institute for Advanced Study. (last accessed date 09/08/2016) · Zbl 1336.00105 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
