Document Open Access Logo

The Yoneda Reduction of Polymorphic Types

Authors Paolo Pistone, Luca Tranchini

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2021.35.pdf
  • Filesize: 0.66 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Program semantics
Keywords
  • System F
  • Type isomorphisms
  • Yoneda isomorphism
  • Program equivalence

Metrics

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

Abstract

In this paper we explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than βη-equivalence, like those induced by parametricity and dinaturality. We show that the Yoneda type isomorphisms yield a rewriting over types, that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We establish some sufficient conditions under which quantifiers can be fully eliminated from a polymorphic type, and we show some application of these conditions to count the inhabitants of a type and to compute program equivalence in some fragments of System F.

Cite As Get BibTex

Paolo Pistone and Luca Tranchini. The Yoneda Reduction of Polymorphic Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CSL.2021.35

Author Details

Paolo Pistone
  • DISI, University of Bologna, Italy
Luca Tranchini
  • Wilhelm-Schickard-Institut, Universität Tübingen, Germany

Funding

  • Pistone, Paolo: ERC CoG 818616 "DIAPASoN".
  • Tranchini, Luca: DFG TR1112/4-1 "Falsity and Refutation. On the negative side of logic".

References

  1. Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. Theorems for free for free: parametricity, with and without types. In Proceedings of the ACM on Programming Languages, volume 1 of ICFP, page Article No. 39, New York, 2017. Google Scholar
  2. T. Aoto. Uniqueness of normal proofs in implicational intuitionistic logic. Journal of Logic, Language and Information, 8:217-242, 1999. Google Scholar
  3. Steve Awodey, Jonas Frey, and Sam Speight. Impredicative encodings of (higher) inductive types. In LICS 2018, 2018. Google Scholar
  4. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative-additive case. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 42:1-42:17, Germany, 2016. Dagstuhl. Google Scholar
  5. E.S. Bainbridge, Peter J. Freyd, Andre Scedrov, and Philip J. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35-64, 1990. Google Scholar
  6. Henning Basold and Helle Hvid Hansen. Well-definedness and observational equivalence for inductive-coinductive programs. Journal of Logic and Computation, exw091, 2016. Google Scholar
  7. Jean-Philippe Bernardy, Patrik Jansson, and Koen Claessen. Testing Polymorphic Properties. In ESOP 2010: Programming Languages and Systems, volume 6012 of Lecture Notes in Computer Science, pages 125-144. Springer Berlin Heidelberg, 2010. Google Scholar
  8. P. Bourreau and S. Salvati. Game semantics and uniqueness of type inhabitance in the simply-typed λ-calculus. In TLCA 2011, volume 6690 of LNCS, pages 61-75. Springer Berlin Heidelberg, 2011. Google Scholar
  9. S. Broda and L. Damas. On long normal inhabitants of a type. Journal of Logic and Computation, 15:353-390, 2005. Google Scholar
  10. Kim B. Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 1:1-20, 1991. Google Scholar
  11. Joachim de Lataillade. Dinatural terms in System F. In Proceedings of the Twenty-Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 2009), pages 267-276, Los Angeles, California, USA, 2009. IEEE Computer Society Press. Google Scholar
  12. Roberto Di Cosmo. A short survey of isomorphisms of types. Mathematical Structures in Computer Science, 15:825-838, 2005. Google Scholar
  13. Fiore, Roberto Di Cosmo, and Vincent Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. Annals of Pure and Applied Logic, 141(1-2):35-50, 2006. Google Scholar
  14. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Structures in Computer Science, 154(1):153-192, 2013. Google Scholar
  15. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Normal forms and cut-free proofs as natural transformations. In Y. Moschovakis, editor, Logic from Computer Science, volume 21, pages 217-241. Springer-Verlag, 1992. Google Scholar
  16. Ryu Hasegawa. Categorical data types in parametric polymorphism. Mathematical Structures in Computer Science, 4(1):71-109, 1994. Google Scholar
  17. Ralf Hinze and Daniel W.H. James. Reason isomorphically! In WGP 2010, pages 85-96, 2010. Google Scholar
  18. Danko Ilik. Axioms and decidability for type isomorphism in the presence of sums. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014. Google Scholar
  19. Patricia Johann. On proving the correctness of program transformation based on free theorems for higher-order polymorphic calculi. Mathematical Structures in Computer Science, 15:201-229, 2005. Google Scholar
  20. Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. PhD thesis, Ludwig-Maximilians-Universität München, 1998. Google Scholar
  21. Guy McCuscker and Alessio Santamaria. On compositionality of dinatural transformations. In CSL 2018, volume 119 of LIPIcs, pages 33:1-33:22, Dagstuhl, Germany, 2018. Schloss Daghstuhl-Leibinz-Zentrum fuer Informatik. Google Scholar
  22. M. Okada and P.J. Scott. A note on rewriting theory for uniqueness of iteration. Theory and Applications of Categories, 6:47-64, 1999. Google Scholar
  23. Paolo Pistone. On dinaturality, typability and βη-stable models. In Schloos Dagstul-Leibniz-Zentrum fuer Informatik, editor, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), volume 84 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1-29:17, Dagstuhl, Germany, 2017. Google Scholar
  24. Paolo Pistone. On completeness and parametricity in the realizability semantics of System F. Logical Methods in Computer Science, 15(4):6:1-6:54, 2019. Google Scholar
  25. Paolo Pistone. Proof nets, coends and the Yoneda isomorphism. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018), volume 292 of EPTCS, pages 148-167, 2019. Google Scholar
  26. Paolo Pistone and Luca Tranchini. The Yoneda Reduction of Polymorphic Types, extended version, 2020. URL: https://arxiv.org/abs/1907.03481.
  27. Paolo Pistone, Luca Tranchini, and Mattia Petrolo. The naturality of natural deduction (II). Some remarks on atomic polymorphism, 2020. URL: https://arxiv.org/abs/1908.11353.
  28. Gordon Plotkin and Martin Abadi. A logic for parametric polymorphism. In TLCA '93, International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 361-375. Springer Berlin Heidelberg, 1993. Google Scholar
  29. Luigi Santocanale. Free μ-lattices. Journal of Pure and Applied Algebra, 9:166-197, 2002. Google Scholar
  30. Gabriel Scherer. Which types have a unique inhabitant? Focusing on pure program equivalence. PhD thesis, Université Paris-Diderot, 2016. Google Scholar
  31. Gabriel Scherer. Deciding equivalence with sums and the empty type. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 374-386, New York, NY, USA, 2017. ACM. Google Scholar
  32. Gabriel Scherer and Didier Rémy. Which simple types have a unique inhabitant? SIGPLAN Not., 50(9):243-255, 2015. Google Scholar
  33. Makoto Tatsuta. Second order permutative conversions with Prawitz’s strong validity. Progress in Informatics, 2:41-56, 2005. Google Scholar
  34. Luca Tranchini, Paolo Pistone, and Mattia Petrolo. The naturality of natural deduction. Studia Logica, 107(1):195-231, 2019. Google Scholar
  35. Tarmo Uustalu and Varmo Vene. The Recursion Scheme from the Cofree Recursive Comonad. Electronic Notes in Theoretical Computer Science, 229(5):135-157, 2011. Google Scholar
  36. Janis Voigtländer. Free theorems simply, via dinaturality. In Declarative Programming and Knowledge Management, pages 247-267, Cham, 2020. Springer International Publishing. Google Scholar
  37. Philip Wadler. Theorems for free! In Proceedings of the fourth international conference on functional programming languages and computer architecture - FPCA '89, 1989. Google Scholar
  38. Marek Zaoinc. Fixpoint technique for counting terms in typed lambda-calculus. Technical report, State University of New York, 1995. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact