Document Open Access Logo

Quantitative Polynomial Functors

Authors Georgi Nakov , Fredrik Nordvall Forsberg

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.10.pdf
  • Filesize: 0.86 MB
  • 22 pages

Document Identifiers

Author Details

Georgi Nakov
  • Department of Computer and Information Sciences, University of Strathclyde, Glasgow, UK
Fredrik Nordvall Forsberg
  • Department of Computer and Information Sciences, University of Strathclyde, Glasgow, UK

Cite As Get BibTex

Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.TYPES.2021.10

Abstract

We investigate containers and polynomial functors in Quantitative Type Theory, and give initial algebra semantics of inductive data types in the presence of linearity. We show that reasoning by induction is supported, and equivalent to initiality, also in the linear setting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Linear logic
Keywords
  • quantitative type theory
  • polynomial functors
  • inductive data types

Metrics

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

Supplementary Materials

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Categories of containers. In Andrew D. Gordon, editor, Foundations of Software Science and Computation Structures, pages 23-38. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_2.
  2. Michael 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.
  3. Andreas Abel and Jean-Philippe Bernardy. A unified view of modalities in type systems. Proceedings of the ACM on Programming Languages, 4(ICFP):1-28, 2020. URL: https://doi.org/10.1145/3408972.
  4. Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science, 12(5):625-665, 2002. URL: https://doi.org/10.1017/S0960129502003730.
  5. 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, Lecture Notes in Computer Science, pages 293-310. Springer, Heidelberg, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_16.
  6. Robert Atkey. Syntax and semantics of quantitative type theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18, pages 56-65. ACM Press, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  7. Steve Awodey, Nicola Gambino, and Kristina Sojakova. Homotopy-initial algebras in type theory. Journal of the ACM, 63(6), 2017. URL: https://doi.org/10.1145/3006383.
  8. Edwin Brady. Idris 2: Quantitative Type Theory in Practice. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming (ECOOP 2021), volume 194 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.9.
  9. Iliano Cervesato and Frank Pfenning. A Linear Logical Framework. Information and Computation, 179(1):19-75, 2002. URL: https://doi.org/10.1006/inco.2001.2951.
  10. Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang., 5(POPL):1-32, 2021. URL: https://doi.org/10.1145/3434331.
  11. 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 fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  12. Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 255-264. Association for Computing Machinery, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  13. Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, COLOG-88, pages 50-66. Springer, 1990. URL: https://doi.org/10.1007/3-540-52335-9_47.
  14. Peter Dybjer. Internal type theory. In Lecture Notes in Computer Science, volume 1158 LNCS, pages 120-134. Springer, Berlin, Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-61780-9_66.
  15. 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.
  16. Peter Dybjer and Anton Setzer. Induction–recursion and initial algebras. Annals of Pure and Applied Logic, 124(1):1-47, 2003. URL: https://doi.org/10.1016/S0168-0072(02)00096-9.
  17. Peng Fu, Kohei Kishida, and Peter Selinger. Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 440-453. Association for Computing Machinery, 2020. URL: https://doi.org/10.1145/3373718.3394765.
  18. Nicola Gambino and Martin Hyland. Wellfounded Trees and Dependent Polynomial Functors. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, TYPES 2003, volume 3085 of Lecture Notes in Computer Science, pages 210-225. Springer, Berlin, Heidelberg, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_14.
  19. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153-192, 2013. URL: https://doi.org/10.1017/S0305004112000394.
  20. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  21. Peter Hancock and Pierre Hyvernat. Programming interfaces and basic topology. Annals of Pure and Applied Logic, 137(1-3):189-239, 2006. URL: https://doi.org/10.1016/j.apal.2005.05.022.
  22. Peter Hancock and Anton Setzer. Interactive Programs in Dependent Type Theory. In Peter Clote and Helmut Schwichtenberg, editors, Computer Science Logic, CSL 2000, volume 1862 of Lecture Notes in Computer Science, pages 317-331. Springer, Berlin, Heidelberg, 2000. URL: https://doi.org/10.1007/3-540-44622-2_21.
  23. 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.
  24. Naohiko Hoshino. Linear Realizability. In Computer Science Logic, volume 4646 LNCS, pages 420-434. Springer, Berlin, Heidelberg, Berlin, Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_32.
  25. Jasper Hugunin. Why not W? In 26th International Conference on Types for Proofs and Programs (TYPES 2020), 2020. https://doi.org/10.4230/LIPIcs.TYPES.2020.8.
  26. Ambrus Kaposi and András Kovács. Signatures and induction principles for higher inductive-inductive types. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:10)2020.
  27. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL):2:1-2:24, 2019. URL: https://doi.org/10.1145/3290315.
  28. András Kovács and Ambrus Kaposi. Large and infinitary quotient inductive-inductive types. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 648-661. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394770.
  29. Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. Integrating Linear and Dependent Types. ACM SIGPLAN Notices, 50(1):17-30, 2015. URL: https://doi.org/10.1145/2775051.2676969.
  30. Peter Lefanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159-208, 2020. URL: https://doi.org/10.1017/S030500411900015X.
  31. Conor McBride. I Got Plenty o' Nuttin'. In Lecture Notes in Computer Science, volume 9600, pages 207-233. Springer Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_12.
  32. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages, 3(ICFP):110:1-110:30, 2019. URL: https://doi.org/10.1145/3341714.
  33. Uday S. Reddy. A linear logic model of state. Manuscript, 1993. Google Scholar
  34. Jan M. Smith. The independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes. Journal of Symbolic Logic, 53(3):840-845, 1988. URL: https://doi.org/10.2307/2274575.
  35. Tomáš Svoboda. Additive pairs in quantitative type theory. Master thesis, Charles University Prague, 2021. URL: https://doi.org/20.500.11956/127263.
  36. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  37. Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods. North Holland, 1990. 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 About DROPS Imprint Privacy Contact