Document Open Access Logo

Data Types as Quotients of Polynomial Functors

Authors Jeremy Avigad , Mario Carneiro , Simon Hudon

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2019.6.pdf
  • Filesize: 0.49 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Theory of computation → Data structures design and analysis
Keywords
  • data types
  • polynomial functors
  • inductive types
  • coinductive types

Metrics

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

Abstract

A broad class of data types, including arbitrary nestings of inductive types, coinductive types, and quotients, can be represented as quotients of polynomial functors. This provides perspicuous ways of constructing them and reasoning about them in an interactive theorem prover.

Cite As Get BibTex

Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data Types as Quotients of Polynomial Functors. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.6

Author Details

Jeremy Avigad
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA
Mario Carneiro
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA
Simon Hudon
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

Work partially supported by AFOSR grant FA9550-18-1-0120 and the Sloan Foundation.

Acknowledgements

We are grateful to Andrei Popescu, Dmitriy Traytel, and Jasmin Blanchette for extensive discussions and very helpful advice.

Supplementary Materials

  • Lean formalizations are online at www.github.com/avigad/qpf.

References

  1. Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. Categories of Containers. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures (FOSSACS) 2003, pages 23-38. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_2.
  2. Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, and Conor McBride. Constructing Polymorphic Programs with Quotient Types. In Dexter Kozen and Carron Shankland, editors, Mathematics of Program Construction (MPC) 2004, pages 2-15. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27764-4_2.
  3. Peter Aczel. Non-well-founded sets. Stanford University, Center for the Study of Language and Information, Stanford, CA, 1988. Google Scholar
  4. Peter Aczel and Nax Mendler. A final coalgebra theorem. In Category theory and computer science, pages 357-365. Springer, Berlin, 1989. URL: https://doi.org/10.1007/BFb0018361.
  5. Jiri Adámek and H.-E. Porst. On tree coalgebras and coalgebra presentations. Theoret. Comput. Sci., 311(1-3):257-283, 2004. URL: https://doi.org/10.1016/S0304-3975(03)00378-5.
  6. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Fixed points of functors. J. Log. Algebr. Methods Program., 95:41-81, 2018. URL: https://doi.org/10.1016/j.jlamp.2017.11.003.
  7. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed containers. J. Funct. Programming, 25:e5, 41, 2015. URL: https://doi.org/10.1017/S095679681500009X.
  8. Jeremy Avigad, Soonho Kong, and Leonardo de Moura. Theorem Proving in Lean. Online documentation. URL: https://leanprover.github.io/theorem_proving_in_lean/.
  9. Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299-315, 1993. URL: https://doi.org/10.1016/0304-3975(93)90076-6.
  10. Henning Basold. Mixed Inductive-Coinductive Reasoning Types, Programs and Logic. PhD thesis, Radboud Universiteit Nijmegen, 2018. Google Scholar
  11. Henning Basold and Herman Geuvers. Type Theory based on Dependent Inductive and Coinductive Types. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Logic in Computer Science (LICS) 2016, pages 327-336. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934514.
  12. Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In Clare Dixon and Marcelo Finger, editors, Frontiers of Combining Systems (FroCoS) 2017, pages 3-21. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66167-4_1.
  13. Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants. In Hongseok Yang, editor, Programming Languages and Systems (ESOP) 2017, pages 111-140. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_5.
  14. Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. Bindings as bounded natural functors. PACMPL, 3(POPL):22:1-22:34, 2019. URL: https://doi.org/10.1145/3290335.
  15. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly Modular (Co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving (ITP) 2014, pages 93-110. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_7.
  16. Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, and Dmitriy Traytel. Foundational nonuniform (Co)datatypes for higher-order logic. In Logic in Computer Science (LICS) 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005071.
  17. Cyril Cohen. Pragmatic Quotient Types in Coq. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving (ITP) 2013, pages 213-228. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_17.
  18. Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986. URL: http://dl.acm.org/citation.cfm?id=10510.
  19. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Conference on Automated Deduction (CADE) 2015, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  20. Richard Dedekind. Was sind und was sollen die Zahlen? Vieweg, Braunschweig, 1888. Translated by Wooster Beman as "The nature and meaning of numbers" in Essays on the theory of numbers, Open Court, Chicago, 1901; reprinted by Dover, New York, 1963. Google Scholar
  21. Peter Dybjer. Inductive Families. Formal Asp. Comput., 6(4):440-465, 1994. URL: https://doi.org/10.1007/BF01211308.
  22. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metaprogramming framework for formal verification. PACMPL, 1(ICFP):34:1-34:29, 2017. URL: https://doi.org/10.1145/3110278.
  23. Denis Firsov and Aaron Stump. Generic derivation of induction for impredicative encodings in Cedille. In June Andronick and Amy P. Felty, editors, Certified Programs and Proofs (CPP) 2018, pages 215-227. ACM, 2018. URL: https://doi.org/10.1145/3167087.
  24. Gottlob Frege. Grundgesetze der Arithmetik. H. Pohle, Jena, Volume 1, 1893, Volume 2, 1903. Google Scholar
  25. 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, pages 210-225. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_14.
  26. Eduardo Giménez. Codifying Guarded Definitions with Recursive Schemes. In Peter Dybjer, Bengt Nordström, and Jan M. Smith, editors, Types for Proofs and Programs (TYPES) 1994, pages 39-59. Springer, 1994. URL: https://doi.org/10.1007/3-540-60579-7_3.
  27. Martin Hofmann. A Simple Model for Quotient Types. In Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin, editors, Typed Lambda Calculi and Applications (TLCA) 1995, pages 216-234. Springer, 1995. URL: https://doi.org/10.1007/BFb0014055.
  28. Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel. A Formalized Hierarchy of Probabilistic System Types (Proof Pearl). In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving (ITP) 2015, pages 203-220. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_13.
  29. Peter V. Homeier. A Design Structure for Higher Order Quotients. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics (TPHOLs) 2005, pages 130-146. Springer, 2005. URL: https://doi.org/10.1007/11541868_9.
  30. André Joyal. Une théorie combinatoire des séries formelles. Adv. in Math., 42(1):1-82, 1981. URL: https://doi.org/10.1016/0001-8708(81)90052-9.
  31. Bronisław Knaster. Un théorème sur les fonctions d'ensembles. Ann. Soc. Polon. Math., 6:133-134, 1928. Google Scholar
  32. Georg Kreisel. Generalized Inductive Definitions. Stanford Report on the Foundations of Analysis (mimeographed), CH. III, Stanford, 1963. Google Scholar
  33. Alexander Kurz and Jiri Velebil. Relation lifting, a survey. J. Log. Algebr. Meth. Program., 85(4):475-499, 2016. URL: https://doi.org/10.1016/j.jlamp.2015.08.002.
  34. Per Martin-Löf. An intuitionistic theory of types: predicative part. In Logic Colloquium 1973, pages 73-118. North-Holland, Amsterdam, 1975. Google Scholar
  35. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL. A proof assistant for higher-order logic. Springer Verlag, Berlin, 2002. Google Scholar
  36. Jan J. M. M. Rutten. Relators and Metric Bisimulations. Electr. Notes Theor. Comput. Sci., 11:252-258, 1998. URL: https://doi.org/10.1016/S1571-0661(04)00063-5.
  37. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  38. Sam Staton. Relating Coalgebraic Notions of Bisimulation. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science (CALCO) 2009, pages 191-205. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03741-2_14.
  39. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math., 5:285-309, 1955. URL: http://projecteuclid.org/euclid.pjm/1103044538.
  40. Enrico Tassi. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. This Proceedings, 2019. Google Scholar
  41. Brent A. Yorgey. Species and functors and types, oh my! In Jeremy Gibbons, editor, Proceedings of the 3rd ACM SIGPLAN Symposium on Haskell, pages 147-158. ACM, 2010. URL: https://doi.org/10.1145/1863523.1863542.
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