License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2021.35
URN: urn:nbn:de:0030-drops-134696
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13469/
Pistone, Paolo ;
Tranchini, Luca
The Yoneda Reduction of Polymorphic Types
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.
BibTeX - Entry
@InProceedings{pistone_et_al:LIPIcs:2021:13469,
author = {Paolo Pistone and Luca Tranchini},
title = {{The Yoneda Reduction of Polymorphic Types}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {35:1--35:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-175-7},
ISSN = {1868-8969},
year = {2021},
volume = {183},
editor = {Christel Baier and Jean Goubault-Larrecq},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13469},
URN = {urn:nbn:de:0030-drops-134696},
doi = {10.4230/LIPIcs.CSL.2021.35},
annote = {Keywords: System F, Type isomorphisms, Yoneda isomorphism, Program equivalence}
}
Keywords: |
|
System F, Type isomorphisms, Yoneda isomorphism, Program equivalence |
Collection: |
|
29th EACSL Annual Conference on Computer Science Logic (CSL 2021) |
Issue Date: |
|
2021 |
Date of publication: |
|
13.01.2021 |