Document Open Access Logo

Impredicative Encodings of Inductive and Coinductive Types

Authors Steven Bronsveld , Herman Geuvers , Niels van der Weide

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.11.pdf
  • Filesize: 1.62 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Formulas-as-types
  • impredicativity
  • inductive types
  • coinductive types

Metrics

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

Abstract

In impredicative type theory (System F, also known as λ2), it is possible to define inductive data types, such as natural numbers and lists. It is also possible to define coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the β-rules). Unfortunately, they do not yield a (co)induction principle [Herman Geuvers, 2001; Ivar Rummelhoff, 2004], because the necessary uniqueness principles are missing (the η-rules). Awodey, Frey, and Speight [Steve Awodey et al., 2018] used an extension of the Calculus of Constructions [Thierry Coquand and Gérard P. Huet, 1988] (λ C) with Σ-types, identity-types, and functional extensionality to define System F style inductive types with an induction principle, by encoding them as a well-chosen subtype, making them initial algebras.
In this paper, we extend their results to coinductive data types, and we detail the example of the stream data type with the desired coinduction principle (also called bisimulation). To do that, we first define quotient types (with the desired η-rules) and we also need a stronger form of the definable existential types. We also show that we can use the original method by Awodey, Frey and Speight for general inductive types by defining W-types with an induction principle. The dual approach for streams can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.

Cite As Get BibTex

Steven Bronsveld, Herman Geuvers, and Niels van der Weide. Impredicative Encodings of Inductive and Coinductive Types. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.11

Author Details

Steven Bronsveld
  • iCIS, Radboud University Nijmegen, The Netherlands
Herman Geuvers
  • iCIS, Radboud University Nijmegen, The Netherlands
  • Technical University Eindhoven, The Netherlands
Niels van der Weide
  • iCIS, Radboud University Nijmegen, The Netherlands

Funding

  • van der Weide, Niels: This research was supported by the NWO project "The Power of Equality" OCENW.M20.380, which is financed by the Dutch Research Council (NWO).

Acknowledgements

We thank Benno van den Berg and Daniel Otten for fruitful discussions. We thank the referees for their valuable comments and suggestions.

References

  1. Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3-27, 2005. URL: https://doi.org/10.1016/J.TCS.2005.06.002.
  2. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in homotopy type theory. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland, volume 38 of LIPIcs, pages 17-30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPICS.TLCA.2015.17.
  3. Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman. Internal parametricity, without an interval. Proc. ACM Program. Lang., 8(POPL):2340-2369, 2024. URL: https://doi.org/10.1145/3632920.
  4. Steve Awodey, Jonas Frey, and Sam Speight. Impredicative encodings of (higher) inductive types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 76-85. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209130.
  5. Steven Awodey, Nicola Gambino, and Kristina Sojakova. Inductive types in homotopy type theory. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 95-104. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.21.
  6. Henk Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125-154, 1991. URL: https://doi.org/10.1017/S0956796800020025.
  7. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of agda - A functional language with dependent types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 73-78. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
  8. Alonzo Church. A formulation of the simple theory of types. J. Symb. Log., 5(2):56-68, 1940. URL: https://doi.org/10.2307/2266170.
  9. Thierry Coquand and Gérard P. Huet. The Calculus of Constructions. Inf. Comput., 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  10. Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, volume 417 of Lecture Notes in Computer Science, pages 50-66. Springer, 1988. URL: https://doi.org/10.1007/3-540-52335-9_47.
  11. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  12. Denis Firsov and Aaron Stump. Generic derivation of induction for impredicative encodings in Cedille. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 215-227. ACM, 2018. URL: https://doi.org/10.1145/3167087.
  13. Herman Geuvers. Induction is not derivable in second order dependent type theory. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, volume 2044 of Lecture Notes in Computer Science, pages 166-181. Springer, 2001. URL: https://doi.org/10.1007/3-540-45413-6_16.
  14. Herman Geuvers. The Church-Scott representation of inductive and coinductive data, 2014. URL: https://api.semanticscholar.org/CorpusID:13897083.
  15. Jean-Yves Girard. Une extension de l'interpretation de Gödel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 63-92. Elsevier, 1971. URL: https://doi.org/10.1016/S0049-237X(08)70843-7.
  16. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Cambridge University Press, 1993. Google Scholar
  17. Claudio Hermida and Bart Jacobs. Structural induction and coinduction in a fibrational setting. Information and Computation, 145(2):107-152, 1998. URL: https://doi.org/10.1006/inco.1998.2725.
  18. Bart Jacobs and Jan Rutten. An introduction to (co)algebra and (co)induction. In Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge tracts in theoretical computer science, pages 38-99. Cambridge University Press, 2012. Google Scholar
  19. Christopher Jenkins, Aaron Stump, and Larry Diehl. Efficient lambda encodings for Mendler-style coinductive types in Cedille. In Max S. New and Sam Lindley, editors, Proceedings Eighth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2020, Dublin, Ireland, 25th April 2020, volume 317 of EPTCS, pages 72-97, 2020. URL: https://doi.org/10.4204/EPTCS.317.5.
  20. Neelakantan R. Krishnaswami and Derek Dreyer. Internalizing relational parametricity in the extensional calculus of constructions. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 432-451. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPICS.CSL.2013.432.
  21. Nuo Li. Quotient Types in Type Theory. PhD thesis, University of Nottingham, 2014. Google Scholar
  22. Per Martin-Löf, 1984. Notes by Giovanni Sambin of a series of lectures in Padua, 1980. Google Scholar
  23. Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof: An Introduction. Cambridge University Press, 2014. Google Scholar
  24. nLab authors. hom-functor preserves limits. https://ncatlab.org/nlab/show/hom-functor+preserves+limits, June 2024. URL: https://ncatlab.org/nlab/revision/hom-functor+preserves+limits/11.
  25. Daniël Otten. M-types and bisimulation. Bachelor’s thesis, Leiden University, 2020. URL: https://theses.liacs.nl/pdf/2019-2020-OttenDD.pdf.
  26. Christine Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In 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: https://doi.org/10.1007/BFB0037116.
  27. Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29 - April 1, 1989, Proceedings, volume 442 of Lecture Notes in Computer Science, pages 209-228. Springer, 1989. URL: https://doi.org/10.1007/BFB0040259.
  28. Felix Rech. Strictly Positive Types in Homotopy Type Theory. Bachelor Thesis, Saarland University, 2017. Google Scholar
  29. John C. Reynolds. Towards a theory of type structure. In Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974, volume 19 of Lecture Notes in Computer Science, pages 408-423. Springer, 1974. URL: https://doi.org/10.1007/3-540-06859-7_148.
  30. Egbert Rijke. Introduction to Homotopy Type Theory, 2022. URL: https://arxiv.org/abs/2212.11082.
  31. Xavier Ripoll Echeveste. Alternative impredicative encodings of inductive types. Master’s thesis, Universiteit van Amsterdam, 2023. Google Scholar
  32. Ivar Rummelhoff. Polynat in PER models. Theor. Comput. Sci., 316(1):215-224, 2004. URL: https://doi.org/10.1016/J.TCS.2004.01.031.
  33. Sam Speight. Impredicative encodings of inductive types in Homotopy Type Theory. Master’s thesis, Carnegie Mellon University, Pittsburgh, USA, 2017. URL: https://www.cs.ox.ac.uk/people/sam.speight/publications/sams-hott-thesis.pdf0.
  34. Rocq Development Team. The Rocq proof assistant, June 2024. URL: https://doi.org/10.5281/zenodo.11551307.
  35. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  36. Benno van den Berg and Federico De Marchi. Non-well-founded trees in categories. Ann. Pure Appl. Logic, 146(1):40-59, 2007. URL: https://doi.org/10.1016/J.APAL.2006.12.001.
  37. Philip Wadler. The Girard-Reynolds isomorphism. Inf. Comput., 186(2):260-284, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00141-X.
  38. Philip Wadler. The Girard-Reynolds isomorphism (second edition). Theoretical Computer Science, 375(1-3):201-226, 2007. URL: https://doi.org/10.1016/J.TCS.2006.12.042.
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