Document Open Access Logo

A Syntax for Higher Inductive-Inductive Types

Authors Ambrus Kaposi , András Kovács

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.20.pdf
  • Filesize: 418 kB
  • 18 pages

Document Identifiers

Author Details

Ambrus Kaposi
  • Faculty of Informatics, Eötvös Loránd University, Pázmány Péter sétány 1/C, 1117 Budapest, Hungary
András Kovács
  • Faculty of Informatics, Eötvös Loránd University, Pázmány Péter sétány 1/C, 1117 Budapest, Hungary

Funding

This work was supported by the European Union, co-financed by the European Social Fund (EFOP-3.6.3-VEKOP-16-2017-00002), USAF grant FA9550-16-1-0029, and by COST Action EUTypes CA15123.

Cite AsGet BibTex

Ambrus Kaposi and András Kovács. A Syntax for Higher Inductive-Inductive Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.20

Abstract

Higher inductive-inductive types (HIITs) generalise inductive types of dependent type theories in two directions. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalising higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy reals and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a domain-specific type theory. A context in this small type theory encodes a HIIT by listing the type formation rules and constructors. The type of the elimination principle and its beta-rules are computed from the context using a variant of the syntactic logical relation translation. We show that for indexed W-types and various examples of HIITs the computed elimination principles are the expected ones. Showing that the thus specified HIITs exist is left as future work. The type theory specifying HIITs was formalised in Agda together with the syntactic translations. A Haskell implementation converts the types of sorts and constructors into valid Agda code which postulates the elimination principles and computation rules.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • homotopy type theory
  • inductive-inductive types
  • higher inductive types
  • quotient inductive types
  • logical relations

Metrics

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

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers - constructing strictly positive types. Theoretical Computer Science, 342:3-27, September 2005. Applied Semantics: Selected Topics. Google Scholar
  2. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures, pages 293-310, Cham, 2018. Springer International Publishing. Google Scholar
  3. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodik and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29. ACM, 2016. URL: http://dl.acm.org/citation.cfm?id=2837614, URL: http://dx.doi.org/10.1145/2837614.2837638.
  4. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In Suresh Jagannathan and Peter Sewell, editors, 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. ACM, 2014. URL: http://dl.acm.org/citation.cfm?id=2535838, URL: http://dx.doi.org/10.1145/2535838.2535852.
  5. Henning Basold and Herman Geuvers. Type Theory based on Dependent Inductive and Coinductive Types. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of LICS '16, pages 327-336. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2934514.
  6. Henning Basold, Herman Geuvers, and Niels van der Weide. Higher inductive types in programming. Journal of Universal Computer Science, 23(1):63-88, jan 2017. Google Scholar
  7. Andrej Bauer, Gaëtan Gilbert, Philipp Haselwarter, Matija Pretnar, and Christopher A. Stone. Design and implementation of the andromeda proof assistant. In Silvia Ghilezan and Ivetić Jelena, editors, 22nd International Conference on Types for Proofs and Programs, TYPES 2016. University of Novi Sad, 2016. Google Scholar
  8. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Parametricity and dependent types. In ACM Sigplan Notices, volume 45, pages 345-356. ACM, 2010. Google Scholar
  9. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Proofs for free - parametricity for dependent types. Journal of Functional Programming, 22(02):107-152, 2012. URL: http://dx.doi.org/10.1017/S0956796812000056.
  10. Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. The next 700 syntactical models of type theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 182-194, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3018610.3018620.
  11. Paolo Capriotti and Nicolai Kraus. Univalent higher categories via complete semi-segal types. Proc. ACM Program. Lang., 2(POPL):44:1-44:29, dec 2017. URL: http://dx.doi.org/10.1145/3158132.
  12. Floris van Doorn. Constructing the propositional truncation using non-recursive hits. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pages 122-129, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2854065.2854076.
  13. Peter Dybjer. Inductive families. Formal Aspects of Computing, 6:440-465, 1997. Google Scholar
  14. Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65:525-549, 2000. Google Scholar
  15. Peter Dybjer and Hugo Moeneclaey. Finitary higher inductive types in the groupoid model. Electronic Notes in Theoretical Computer Science, 336:119-134, 2018. The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII). URL: http://dx.doi.org/10.1016/j.entcs.2018.03.019.
  16. Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129-146. Springer, 1999. Google Scholar
  17. Martin Hofmann. Extensional concepts in intensional type theory. Thesis. University of Edinburgh, Department of Computer Science, 1995. Google Scholar
  18. Ambrus Kaposi. Type theory in a type theory with quotient inductive types. PhD thesis, University of Nottingham, 2017. Google Scholar
  19. Nicolai Kraus. Constructions with non-recursive higher inductive types. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 595-604, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2933575.2933586.
  20. Marc Lasson. Canonicity of weak ω-groupoid laws using parametricity theory. Electronic Notes in Theoretical Computer Science, 308:229-244, 2014. URL: http://dx.doi.org/10.1016/j.entcs.2014.10.013.
  21. Peter LeFanu Lumsdaine and Mike Shulman. Semantics of higher inductive types, 2017. URL: http://arxiv.org/abs/1705.07088.
  22. Peter Morris and Thorsten Altenkirch. Indexed containers. In Twenty-Fourth IEEE Symposium in Logic in Computer Science (LICS 2009), 2009. Google Scholar
  23. Fredrik Nordvall Forsberg. Inductive-inductive definitions. PhD thesis, Swansea University, 2013. Google Scholar
  24. Christine Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 328-345. Springer, 1993. URL: http://dx.doi.org/10.1007/BFb0037116.
  25. The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. Technical report, Institute for Advanced Study, 2013. Google Scholar
  26. Kristina Sojakova. Higher inductive types as homotopy-initial algebras. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 31-42, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2676726.2676983.
  27. Niels van der Weide. Higher inductive types. Master’s thesis, Radboud University, Nijmegen, 2016. Google Scholar
  28. Vladimir Voevodsky. A simple type system with two identity types. Unpublished note, 2013. Google Scholar
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