Document Open Access Logo

Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism

Author James Laird

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.33.pdf
  • Filesize: 0.77 MB
  • 16 pages

Document Identifiers

Author Details

James Laird
  • Department of Computer Science, University of Bath, UK

Cite AsGet BibTex

James Laird. Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.33

Abstract

We study subtyping and parametric polymorphism, with the aim of providing direct and tractable semantic representations of type systems with these expressive features. The liveness order uses the Player-Opponent duality of game semantics to give a simple representation of subtyping: we generalize it to include graphs extracted directly from second-order intuitionistic types, and use the resulting complete lattice to interpret bounded polymorphic types in the style of System F_<:, but with a more tractable subtyping relation. To extend this to a semantics of terms, we use the type-derived graphs as arenas, on which strategies correspond to dinatural transformations with respect to the canonical coercions ("on the nose" copycats) induced by the liveness ordering. This relationship between the interpretation of generic and subtype polymorphism thus provides the basis of the semantics of our type system.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • Subtyping
  • Bounded Polymorphism
  • Game Semantics
  • Dinaturality

Metrics

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

References

  1. E. S. Bainbridge, P. J. Freyd, A. Scedrov, and P.J. Scott. Functorial polymorphism. Theoretical Computer Science, 70(1):35-64, 1990. URL: https://doi.org/10.1016/0304-3975(90)90055-m.
  2. K. Bruce and G. Longo. A modest model of records, inheritance and bounded quantification. Information and Computation, 87(1/2):196-240, 1990. URL: https://doi.org/10.1109/lics.1988.5099.
  3. L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. Computing Surveys, 17(4):471-522, 1985. Google Scholar
  4. Luca Cardelli, John C. Mitchell, Simone Martini, and Andre Scedrov. An extension of System F with subtyping. Information and Computation, 109(1-2):4-56, 1994. Google Scholar
  5. G. Castagna and B. C. Pierce. Decidable bounded quantification. In Proceedings of POPL '94, pages 1-29, 1994. URL: https://doi.org/10.1145/174675.177844.
  6. J. Chroboczek. Game semantics and subtyping. In Proceedings of the fifteenth annual symposium on Logic in Computer Science, pages 192-203. IEEE press, 2000. URL: https://doi.org/10.1109/lics.2000.855769.
  7. P.-L. Curien and G. Ghelli. Coherence of subsumption, minimum typing and type-checking in F_<:. Mathematical Structures in Computer Science, 2(1):55-91, 1992. URL: https://doi.org/10.1007/3-540-52590-4_45.
  8. J. de Lataillade. Dinatural terms in System F. In Proceedings of the 24th annual symposium on Logic in Computer Science, LICS '09. IEEE Press, 2009. URL: https://doi.org/10.1109/lics.2009.30.
  9. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987. Google Scholar
  10. J. Z. S. Hu and O. Lhoták. Undecidability of D_<: and its decidable fragments. Proceedings of the ACM on Programming Languages (POPL), 4(9):1-30, 2020. URL: https://doi.org/10.1145/3371077.
  11. J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. Information and Computation, 163:285-408, 2000. Google Scholar
  12. D. Katiyar and S. Sankar. Completely bounded quantification is decidable. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, pages 68-77, 1992. Google Scholar
  13. J. Laird. Game semantics for a polymorphic programming language. In Proceedings of LICS '10. IEEE Press, 2010. Google Scholar
  14. J. Laird. Game semantics for a polymorphic programming language. Journal of the ACM, 60(4), 2013. Google Scholar
  15. J. Laird. Game semantics for bounded polymorphism. In Proceedings of FoSSaCS '16, number 9634 in LNCS. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_4.
  16. J. Laird. Revisiting decidable bounded quantification, via dinaturality. In Proceedings of Mathematical Foundations of Program Semantics '22, Electronic Notes in Theoretical Computer Science, 2022. To appear. Google Scholar
  17. N. Amin, S. Grütter, M. Odersky, T. Rompf, and S. Stucki. The essence of dependent object types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, number 9600 in LNCS, pages 249-272. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_14.
  18. B. C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, 1991. URL: https://dl.acm.org/doi/10.5555/145640.
  19. Benjamin C. Pierce. Bounded quantification is undecidable. In POPL, pages 305-315, 1992. URL: https://doi.org/10.1006/inco.1994.1055.
  20. A. M. Pitts. Relational properties of domains. Information and Computation, 127:66-90, 1996. Google Scholar
  21. J. C. Reynolds. Syntactic Control of Interference. In Conf. Record 5^th ACM Symposium on Principles of Programming Languages, pages 39-46, 1978. Google Scholar
  22. Tiark Rompf and Nada Amin. From F to DOT: type soundness proofs with definitional interpreters. CoRR, abs/1510.05216, 2015. URL: https://arxiv.org/abs/1510.05216.
  23. Sergei Vorobyov. Structural decidable extensions of bounded quantification. In Proceedings of POPL '95, pages 164-175, 1995. URL: https://doi.org/10.1145/199448.199479.
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