Document Open Access Logo

Categorical Models of Subtyping

Authors Greta Coraglia , Jacopo Emmenegger

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2023.3.pdf
  • Filesize: 0.85 MB
  • 19 pages

Document Identifiers

Author Details

Greta Coraglia
  • Dipartimento di Filosofia (LUCI Lab), Dipartimento di Eccellenza 2023-2027, Università degli Studi di Milano, Italy
Jacopo Emmenegger
  • Dipartimento di Matematica (DIMA), Dipartimento di Eccellenza 2023-2027, Università degli Studi di Genova, Italy

Funding

  • Coraglia, Greta: The research has been partially funded by the Project PRIN2020 "BRIO" (2020SSKZ7R) awarded by the Italian Ministry of University and Research.
  • Emmenegger, Jacopo: The research has been partially funded by the the Italian Ministry of University and Research under the scheme "Young Researchers" with agreement number SOE_0000071.

Acknowledgements

The first author would like to thank the University of Genoa, where some of this research was completed. We are deeply grateful to Francesco Dagnino, who suggested coercive subtyping in the first place, for his immense clarity of thought. This work benefitted from a lovely visit to LAMA at Université Savoie Mont Blanc in November 2023, and the first author is for it indebted to Tom Hirschowitz and Peio Borthelle, and to the whole group there. Finally, we would like to thank Luca Mesiti for encouraging we explore the monad underlying our structure.

Cite AsGet BibTex

Greta Coraglia and Jacopo Emmenegger. Categorical Models of Subtyping. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.TYPES.2023.3

Abstract

Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context - and for each type a set of terms of said type. This is the case for categories with families, categories with attributes, and natural models; in particular, all of them can be traced back to certain discrete Grothendieck fibrations. We extend this intuition to the case of general, not necessarily discrete, fibrations, so that over a given context one has not only a set but a category of types. We argue that the added structure can be attributed to a notion of subtyping that shares many features with that of coercive subtyping, in the sense that it is the product of thinking about subtyping as an abbreviation mechanism: we say that a given type A' is a subtype of A if there is a unique coercion from A' to A. Whenever we need a term of type A, then, it suffices to have a term of type A', which we can "plug-in" into A. For this version of subtyping we provide rules, coherences, and explicit models, and we compare and contrast it to coercive subtyping as introduced by Z. Luo and others. We conclude by suggesting how the tools we present can be employed in finding appropriate rules relating subtyping and certain type constructors.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
Keywords
  • dependent types
  • subtyping
  • coercive subtyping
  • categorical semantics
  • categories with families
  • monad

Metrics

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

Related Versions

References

  1. Thorsten Altenkirch and Conor McBride. Towards Observational Type Theory. Manuscript, available at https://www.cs.nott.ac.uk/~psztxa/publ/ott-conf.pdf, 2006.
  2. Steve Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science, 28(2):241-286, 2018. URL: https://doi.org/10.1017/S0960129516000268.
  3. Francis Borceux. Handbook of Categorical Algebra, volume 2 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994. URL: https://doi.org/10.1017/CBO9780511525865.
  4. Greta Coraglia. Categorical structures for deduction. PhD thesis, Università degli Studi di Genova, 2023. URL: https://hdl.handle.net/11567/1134175.
  5. Greta Coraglia and Ivan Di Liberti. Context, judgement, deduction, 2021. URL: https://arxiv.org/abs/2111.09438.
  6. Greta Coraglia and Jacopo Emmenegger. A 2-categorical analysis of context comprehension, 2024. URL: https://arxiv.org/abs/2403.03085.
  7. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, pages 120-134, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-61780-9_66.
  8. Jacopo Emmenegger, Luca Mesiti, Giuseppe Rosolini, and Thomas Streicher. A comonad for Grothendieck fibrations. Theory and Applications of Categories, 40:371-389, 2023. Google Scholar
  9. Alexander Grothendieck. Categoriés fibrées et descente (Exposé VI). Revêtements étales et groupe fondamental - SGA1, 1960-61. Google Scholar
  10. J. Martin E. Hyland. The Effective Topos. In A.S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 165-216. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70129-6.
  11. Bart Jacobs. Comprehension categories and the semantics of type dependency. Theoretical Computer Science, 107(2):169-207, 1993. URL: https://doi.org/10.1016/0304-3975(93)90169-T.
  12. Bart Jacobs. Categorical logic and type theory. Elsevier, 1999. Google Scholar
  13. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium: Volume 1. Oxford University Press, 2002. Google Scholar
  14. Anders Kock and Gonzalo E. Reyes. Doctrines in categorical logic. In Studies in Logic and the Foundations of Mathematics, volume 90, pages 283-313. Elsevier, 1977. URL: https://doi.org/10.1016/S0049-237X(08)71104-2.
  15. Joachim Lambek and Philip J. Scott. Introduction to Higher Order Categorical Logic, volume 7 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1986. Google Scholar
  16. F. William Lawvere. Functorial Semantics of Algebraic Theories and Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, 1963. Available as Reprints in Theory and Applications of Categories, No. 5 (2004) pp 1-121 at URL: http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html.
  17. F.W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In A. Heller, editor, Proc. New York Symposium on Application of Categorical Algebra, pages 1-14. Amer.Math.Soc., 1970. Google Scholar
  18. Rodolphe Lepigre and Christophe Raffalli. Practical subtyping for Curry-style languages. ACM Trans. Program. Lang. Syst., 41(1):5:1-5:58, 2019. URL: https://doi.org/10.1145/3285955.
  19. Daniel R. Licata and Robert Harper. 2-dimensional directed type theory. Electronic Notes in Theoretical Computer Science, 276:263-289, 2011. Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII). URL: https://doi.org/10.1016/j.entcs.2011.09.026.
  20. Zhen Lin Low. Logic in a topos, 2013. Manuscript, available at URL: http://zll22.user.srcf.net/talks/2013-01-24-InternalLogic.pdf.
  21. Zhaohui Luo. Coercive subtyping. Journal of Logic and Computation, 9(1):105-130, 1999. URL: https://doi.org/10.1093/logcom/9.1.105.
  22. Zhaohui Luo, Sergei Soloviev, and Tao Xue. Coercive subtyping: Theory and implementation. Information and Computation, 223:18-42, 2013. URL: https://doi.org/10.1016/j.ic.2012.10.020.
  23. Maria E. Maietti and Giuseppe Rosolini. Quotient completion for the foundation of constructive mathematics. Logica Universalis, 7(3):371-402, 2013. URL: https://doi.org/10.1007/s11787-013-0080-2.
  24. Michael Makkai. The fibrational formulation of intuitionistic predicate logic I: completeness according to Gödel, Kripke, and Läuchli, part 2. Notre Dame J. Formal Log., 34:471-498, 1993. URL: https://doi.org/10.1305/ndjfl/1093633902.
  25. Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. SIGPLAN Not., 50(1):3-16, January 2015. URL: https://doi.org/10.1145/2775051.2676970.
  26. David Jaz Myers. Cartesian factorization systems and Grothendieck fibrations, 2020. URL: https://arxiv.org/abs/2006.14022.
  27. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Google Scholar
  28. Edmund Robinson and Giuseppe Rosolini. Colimit completions and the effective topos. The Journal of Symbolic Logic, 55(2):678-699, 1990. URL: https://doi.org/10.2307/2274658.
  29. Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages. Technical Report PRG06, OUCL, August 1971. Available at URL: https://www.cs.ox.ac.uk/publications/publication3723-abstract.html.
  30. Thomas Streicher. Fibred categories à la Jean Bénabou, 2022. URL: https://arxiv.org/abs/1801.02927.
  31. Benno van den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, October 2010. URL: https://doi.org/10.1112/plms/pdq026.
  32. Noam Zeilberger. Principles of type refinement, 2016. Notes of lectures at the Oregon Programming Language Summer School 2016, available at URL: http://noamz.org/oplss16/refinements-notes.pdf.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact