TY - GEN
T1 - Dinaturality Meets Genericity
T2 - 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023
AU - Laird, James
PY - 2023/6/28
Y1 - 2023/6/28
N2 - 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.
AB - 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.
KW - Bounded Polymorphism
KW - Dinaturality
KW - Game Semantics
KW - Subtyping
UR - http://www.scopus.com/inward/record.url?scp=85165998067&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSCD.2023.33
DO - 10.4230/LIPIcs.FSCD.2023.33
M3 - Chapter in a published conference proceeding
AN - SCOPUS:85165998067
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023
A2 - Gaboardi, Marco
A2 - van Raamsdonk, Femke
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Y2 - 3 July 2023 through 6 July 2023
ER -