Document Open Access Logo

Why Not W?

Author Jasper Hugunin

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.8.pdf
  • Filesize: 0.64 MB
  • 9 pages

Document Identifiers

Author Details

Jasper Hugunin
  • Carnegie Mellon University, Pittsburgh, PA, USA

Acknowledgements

I want to thank Jon Sterling and the anonymous reviewers for their helpful feedback.

Cite AsGet BibTex

Jasper Hugunin. Why Not W?. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 8:1-8:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.8

Abstract

In an extensional setting, 𝚆 types are sufficient to construct a broad class of inductive types, but in intensional type theory the standard construction of even the natural numbers does not satisfy the required induction principle. In this paper, we show how to refine the standard construction of inductive types such that the induction principle is provable and computes as expected in intensional type theory without using function extensionality. We extend this by constructing from 𝚆 an internal universe of codes for inductive types, such that this universe is itself an inductive type described by a code in the next larger universe. We use this universe to mechanize and internalize our refined construction.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • dependent types
  • intensional type theory
  • inductive types
  • W types

Metrics

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

Supplementary Materials

References

  1. Thorsten Altenkirch. Extensional equality in intensional type theory. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 412-420. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782636.
  2. Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In Aaron Stump and Hongwei Xi, editors, Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007, pages 57-68. ACM, 2007. URL: https://doi.org/10.1145/1292597.1292608.
  3. Marcin Benke, Peter Dybjer, and Patrik Jansson. Universes for generic programs and proofs in dependent type theory. Nord. J. Comput., 10(4):265-289, 2003. Google Scholar
  4. James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. The gentle art of levitation. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 3-14. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863547.
  5. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  6. Peter Dybjer. Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. Theoretical Computer Science, 176(1):329-335, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00145-4.
  7. Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 129-146. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_11.
  8. Neil Ghani, Conor McBride, Fredrik Nordvall Forsberg, and Stephan Spahn. Variations on inductive-recursive definitions. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark, volume 83 of LIPIcs, pages 63:1-63:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.63.
  9. Jean-Yves Girard. Proofs and Types. Cambridge University Press, 1990. Translated and with appendices by Paul Taylor and Yves Lafont. URL: http://www.paultaylor.eu/stable/prot.pdf.
  10. Healfdene Goguen and Zhaohui Luo. Inductive data types: Well-ordering types revisited. Logical Environments, 1992. URL: https://www.cs.rhul.ac.uk/home/zhaohui/WTYPES93.pdf.
  11. Martin Hoffman. Extensional Constructs in Intensional Type Theory. PhD thesis, University of Edinburgh, 1995. Google Scholar
  12. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by G. Sambin of a series of lectures given in Padua, 1980. Google Scholar
  13. Conor McBride. W-types: good news and bad news, March 2010. URL: https://mazzo.li/epilogue/index.html%3Fp=324.html.
  14. Bengt Nordsrtöm, Kent Petersson, and Jan Smith. Programming in Martin-Löf’s Type Theory. Oxford University Press, 1990. Google Scholar
  15. Erik Palmgren. From type theory to setoids and back, 2019. URL: http://arxiv.org/abs/1909.01414.
  16. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
  17. The Coq Development Team. The Coq proof assistant, version 8.12.0, 2020. URL: https://doi.org/10.5281/zenodo.4021912.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact