Cubical agda: a dependently typed programming language with univalence and higher inductive types | Proceedings of the ACM on Programming Languages
- ️AbelAndreas
- ️Fri Jul 26 2019
Article No.: 87, Pages 1 - 29
Abstract
Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.
Supplementary Material
WEBM File (a87-vezzosi.webm)
- Download
- 95.56 MB
References
[1]
Andreas Abel, Joakim Öhman, and Andrea Vezzosi. 2017. Decidability of Conversion for Type Theory in Type Theory. Proc. ACM Program. Lang. 2, POPL, Article 23 (Dec. 2017), 29 pages.
[2]
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming Infinite Structures by Observations. SIGPLAN Not. 48, 1 (Jan. 2013), 27–38.
[3]
Agda development team. 2018. Agda 2.5.4.2 documentation. http://agda.readthedocs.io/en/v2.5.4.2/
[4]
Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. 2015. Non-wellfounded trees in Homotopy Type Theory. CoRR abs/1504.02949 (2015). http://arxiv.org/abs/1504.02949
[5]
Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. (2006). Unpublished draft.
[6]
Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. 2007. Observational Equality, Now!. In PLPV ’07: Proceedings of the 2007 workshop on Programming languages meets program verification. ACM, New York, NY, USA, 57–68.
[7]
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. 2019. Syntax and Models of Cartesian Cubical Type Theory. (February 2019). https://github.com/dlicata335/cart-cube Preprint.
[8]
Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. 2017. Computational Higher Type Theory III: Univalent Universes and Exact Equality. (2017). Preprint arXiv:1712.01800v1.
[9]
Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. 2018. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (Leibniz International Proceedings in Informatics (LIPIcs)), Dan Ghica and Achim Jung (Eds.), Vol. 119. Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1–6:17.
[10]
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, and Robert Harper. 2016. Homotopical patch theory. Journal of Functional Programming 26 (2016).
[11]
Danil Annenkov, Paolo Capriotti, and Nicolai Kraus. 2017. Two-Level Type Theory and Applications. (2017). https://arxiv. org/abs/1705.03307
[12]
Mark Bickford. 2018. Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. CoRR abs/1806.06114 (2018). arXiv: 1806.06114 http://arxiv.org/abs/1806.06114
[13]
Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.
[14]
Guillaume Brunerie. 2016. On the homotopy groups of spheres in homotopy type theory. Ph.D. Dissertation. Université de Nice.
[15]
Evan Cavallo and Robert Harper. 2019. Higher Inductive Types in Cubical Computational Type Theory. Proc. ACM Program. Lang. 3, POPL, Article 1 (Jan. 2019), 27 pages.
[16]
Shumo Chu, Konstantin Weitz, Alvin Cheung, and Dan Suciu. 2017. HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics. SIGPLAN Not. 52, 6 (June 2017), 510–524.
[17]
Jesper Cockx and Andreas Abel. 2018. Elaborating Dependent (Co)Pattern Matching. Proc. ACM Program. Lang. 2, ICFP, Article 75 (July 2018), 30 pages.
[18]
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2015. Cubicaltt. (2015). https://github.com/mortberg/ cubicaltt .
[19]
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Types for Proofs and Programs (TYPES 2015) (LIPIcs), Vol. 69. 5:1–5:34.
[20]
Cyril Cohen, Maxime Dénès, and Anders Mörtberg. 2013. Refinements for Free!. In Certified Programs and Proofs (Lecture Notes in Computer Science), Georges Gonthier and Michael Norrish (Eds.), Vol. 8307. Springer International Publishing, 147–162.
[21]
Thierry Coquand and Nils Anders Danielsson. 2013. Isomorphism is equality. Indagationes Mathematicae 24, 4 (2013), 1105–1120.
[22]
Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). ACM, New York, NY, USA, 255–264.
[23]
Thierry Coquand, Simon Huber, and Christian Sattler. 2019. Homotopy canonicity for cubical type theory. (2019). Preprint available at http://www.cse.chalmers.se/ simonhu/papers/can.pdf.
[24]
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover. In Automated Deduction - CADE-25, 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings.
[25]
Simon Huber. 2016. Canonicity for Cubical Type Theory. (2016). Preprint arXiv:1607.04156.
[26]
Simon Huber. 2017. A Cubical Type Theory for Higher Inductive Types. (2017). http://www.cse.chalmers.se/~simonhu/ misc/hcomp.pdf
[27]
Chris Kapulkin and Peter LeFanu Lumsdaine. 2012. The Simplicial Model of Univalent Foundations (after Voevodsky). (Nov. 2012). Preprint arXiv:1211.2851v4.
[28]
Daniel R. Licata and Guillaume Brunerie. 2015. A Cubical Approach to Synthetic Homotopy Theory. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’15. ACM, 92–103.
[29]
Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. 2018. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK (LIPIcs), Hélène Kirchner (Ed.), Vol. 108. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 22:1–22:17.
[30]
Daniel R. Licata and Michael Shulman. 2013. Calculating the Fundamental Group of the Circle in Homotopy Type Theory. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’13). 223–232.
[31]
Peter LeFanu Lumsdaine and Michael Shulman. 2017. Semantics of higher inductive types. (May 2017). Preprint arXiv:1705.07088.
[32]
Per Martin-Löf. 1975. An Intiutionistic Theory of Types: Predicative Part. In Logic Colloquium ’73, H. E. Rose and J. Shepherdson (Eds.). North–Holland, Amsterdam, 73–118.
[33]
Conor McBride. 2009. Let’s See How Things Unfold: Reconciling the Infinite with the Intensional. In Proceedings of the 3rd International Conference on Algebra and Coalgebra in Computer Science (CALCO’09). Springer-Verlag, Berlin, Heidelberg, 113–126. http://dl.acm.org/citation.cfm?id=1812941.1812953
[34]
Ian Orton and Andrew M. Pitts. 2016. Axioms for Modelling Cubical Type Theory in a Topos. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) (LIPIcs), Vol. 62. 24:1–24:19.
[35]
Emily Riehl and Michael Shulman. 2017. A type theory for synthetic ∞-categories. Higher Structures 1, 1 (2017), 147–224.
[36]
Kristina Sojakova. 2016. The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory. ACM Transactions on Computational Logic 17, 4 (Nov. 2016), 29:1–29:19.
[37]
Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. 2019. Cubical Syntax for Reflection-Free Extensional Equality. (2019). http://www.jonmsterling.com/pdfs/xtt.pdf
[38]
Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. 2018. Equivalences for Free: Univalent Parametricity for Effective Transport. Proc. ACM Program. Lang. 2, ICFP, Article 92 (July 2018), 29 pages.
[39]
The Coq Development Team. 2019. The Coq Proof Assistant, version 8.9.0.
[40]
The RedPRL Development Team. 2018. The red tt Proof Assistant. https://github.com/RedPRL/redtt/
[41]
The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.
[42]
Andrea Vezzosi. 2017. Streams for Cubical Type Theory. (2017). http://saizan.github.io/streams-ctt.pdf .
[43]
Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). https://www.math.ias.edu/vladimir/sites/ math.ias.edu.vladimir/files/HTS.pdf
[44]
Vladimir Voevodsky. 2015. An experimental library of formalized Mathematics based on the univalent foundations. Mathematical Structures in Computer Science 25 (2015), 1278–1294.
Information & Contributors
Information
Published In
Proceedings of the ACM on Programming Languages Volume 3, Issue ICFP
August 2019
1054 pages
Copyright © 2019 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 26 July 2019
Published in PACMPL Volume 3, Issue ICFP
Permissions
Request permissions for this article.
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- VR
- Vetenskapsrådet
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- Downloads (Last 12 months)417
- Downloads (Last 6 weeks)60
Reflects downloads up to 03 Mar 2025
Other Metrics
Citations
- Stassen PMøgelberg RZwart MAguirre ABirkedal L(2025)Modelling Recursion and Probabilistic Choice in Guarded Type TheoryProceedings of the ACM on Programming Languages10.1145/37048849:POPL(1417-1445)Online publication date: 9-Jan-2025
- Alexandru CChoudhury VRot Jvan der Weide NStark KTimany ABlazy STabareau N(2025)Intrinsically Correct Sorting in Cubical AgdaProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705873(34-49)Online publication date: 10-Jan-2025
- Goranson TCardier BHancock MEvangelou-Oost NSeligmann BGarcia MSmith G(2025)User affordances to engineer open-world enterprise dynamicsInterdependent Human-Machine Teams10.1016/B978-0-443-29246-0.00006-7(145-174)Online publication date: 2025
- Ahrens BMatthes Rvan der Weide NWullaert KTimany ATraytel DPientka BBlazy S(2024)Displayed Monoidal Categories for the Semantics of Linear LogicProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636956(260-273)Online publication date: 9-Jan-2024
- Eremondi JTimany ATraytel DPientka BBlazy S(2024)Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple ArgumentsProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636948(205-217)Online publication date: 9-Jan-2024
- Kidney DYang ZWu N(2024)Algebraic Effects Meet Hoare Logic in Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328988:POPL(1663-1695)Online publication date: 5-Jan-2024
- Li DChang JHong J(2024)Toward a comprehensive life-cycle carcinogenic impact assessment: A statistical regression approach based on cancer burdenScience of The Total Environment10.1016/j.scitotenv.2024.170851921(170851)Online publication date: Apr-2024
- Myers DSati HSchreiber U(2024)Topological Quantum Gates in Homotopy Type TheoryCommunications in Mathematical Physics10.1007/s00220-024-05020-8405:7Online publication date: 8-Jul-2024
- Pujet LTabareau N(2024)Observational Equality Meets CICProgramming Languages and Systems10.1007/978-3-031-57262-3_12(275-301)Online publication date: 6-Apr-2024
- Cohen CCrance EMahboubi A(2024)Trocq: Proof Transfer for Free, With or Without UnivalenceProgramming Languages and Systems10.1007/978-3-031-57262-3_10(239-268)Online publication date: 6-Apr-2024
- Show More Cited By
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.