Document Open Access Logo

Internal Parametricity for Cubical Type Theory

Authors Evan Cavallo , Robert Harper

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2020.13.pdf
  • Filesize: 0.66 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • parametricity
  • cubical type theory
  • higher inductive types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.

Cite As Get BibTex

Evan Cavallo and Robert Harper. Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.13

Author Details

Evan Cavallo
  • Carnegie Mellon University, Pittsburgh, PA, USA
Robert Harper
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

We gratefully acknowledge the support of the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR.

Acknowledgements

We thank Carlo Angiuli, Steve Awodey, Daniel Gratzer, Kuen-Bang Hou (Favonia), Dan Licata, Anders Mörtberg, Emily Riehl, Christian Sattler, and Jonathan Sterling for their comments and insights.

References

  1. Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, and Philip Wadler. Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically. Submitted to the Journal of Functional Programming, February 2018. URL: https://jesper.sikanda.be/files/leibniz-equality.pdf.
  2. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. Syntax and Models of Cartesian Cubical Type Theory. Unpublished draft, February 2019. URL: https://github.com/dlicata335/cart-cube.
  3. Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, pages 6:1-6:17, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.6.
  4. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 503-516, 2014. URL: https://doi.org/10.1145/2535838.2535852.
  5. Nick Benton, Martin Hofmann, and Vivek Nigam. Abstract effects and proof-relevant logical relations. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 619-632, 2014. URL: https://doi.org/10.1145/2535838.2535869.
  6. Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. A Presheaf Model of Parametric Type Theory. Electr. Notes Theor. Comput. Sci., 319:67-82, 2015. URL: https://doi.org/10.1016/j.entcs.2015.12.006.
  7. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Parametricity and dependent types. In ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 345-356, 2010. Google Scholar
  8. Jean-Philippe Bernardy and Guilhem Moulin. A Computational Interpretation of Parametricity. In LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 135-144, 2012. URL: https://doi.org/10.1109/LICS.2012.25.
  9. Jean-Philippe Bernardy and Guilhem Moulin. Type-theory in color. In ICFP 2013, Boston, MA, USA - September 25 - 27, 2013, pages 61-72, 2013. URL: https://doi.org/10.1145/2500365.2500577.
  10. Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France, pages 107-128, 2013. URL: https://doi.org/10.4230/LIPIcs.TYPES.2013.107.
  11. Marc Bezem, Thierry Coquand, and Simon Huber. The Univalence Axiom in Cubical Sets. J. Autom. Reasoning, 63(2):159-171, 2019. URL: https://doi.org/10.1007/s10817-018-9472-6.
  12. Guillaume Brunerie. Computer-generated proofs for the monoidal structure of the smash product. Homotopy Type Theory Electronic Seminar Talks, November 2018. URL: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html.
  13. Ulrik Buchholtz and Edward Morehouse. Varieties of Cubical Sets. In Relational and Algebraic Methods in Computer Science - 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings, pages 77-92, 2017. URL: https://doi.org/10.1007/978-3-319-57418-9_5.
  14. Evan Cavallo and Robert Harper. Higher inductive types in cubical computational type theory. PACMPL, 3(POPL):1:1-1:27, 2019. URL: https://doi.org/10.1145/3290314.
  15. Evan Cavallo and Robert Harper. Parametric Cubical Type Theory, 2019. URL: http://arxiv.org/abs/1901.00489.
  16. James Cheney. A dependent nominal type theory. Logical Methods in Computer Science, 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:8)2012.
  17. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pages 5:1-5:34, 2015. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  18. Thierry Coquand, Simon Huber, and Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory. In LICS 2018, Oxford, UK, July 9-12, 2018, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  19. Neil Ghani, Patricia Johann, Fredrik Nordvall Forsberg, Federico Orsanigo, and Tim Revell. Bifibrational Functorial Semantics of Parametric Polymorphism. Electr. Notes Theor. Comput. Sci., 319:165-181, 2015. URL: https://doi.org/10.1016/j.entcs.2015.12.011.
  20. Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83-111. Oxford Univ. Press, New York, 1998. Google Scholar
  21. Guilhem Moulin. Internalizing Parametricity. PhD thesis, Chalmers University of Technology, Gothenburg, Sweden, 2016. URL: https://research.chalmers.se/en/publication/235758.
  22. Andreas Nuyts and Dominique Devriese. Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 779-788, 2018. URL: https://doi.org/10.1145/3209108.3209119.
  23. Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. Parametric quantifiers for dependent type theory. PACMPL, 1(ICFP):32:1-32:29, 2017. URL: https://doi.org/10.1145/3110276.
  24. Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science, 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:23)2018.
  25. John C. Reynolds. Types, Abstraction and Parametric Polymorphism. In IFIP Congress, pages 513-523, 1983. Google Scholar
  26. Emily Riehl. On the directed univalence axiom. Talk slides, AMS Special Session on Homotopy Type Theory, Joint Mathematics Meetings, January 2018. URL: http://www.math.jhu.edu/~eriehl/JMM2018-directed-univalence.pdf.
  27. Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures, 1(1):116-193, 2017. URL: https://journals.mq.edu.au/index.php/higher_structures/article/view/36.
  28. Kristina Sojakova and Patricia Johann. A General Framework for Relational Parametricity. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 869-878, 2018. URL: https://doi.org/10.1145/3209108.3209141.
  29. The RedPRL Development Team. redtt, 2018. URL: https://github.com/RedPRL/redtt.
  30. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  31. Floris van Doorn. On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. PhD thesis, Carnegie Mellon University, 2018. Google Scholar
  32. Vladimir Voevodsky. The equivalence axiom and univalent models of type theory, 2014. Talk at CMU on February 4, 2010. URL: http://arxiv.org/abs/1402.5556.
  33. Philip Wadler. Theorems for Free! In FPCA 1989, London, UK, September 11-13, 1989, pages 347-359, 1989. URL: https://doi.org/10.1145/99370.99404.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact