Curry-style type Isomorphisms and Game Semantics
Joachim De Lataillade (PPS)

TL;DR
This paper characterizes type isomorphisms in Curry-style system F using a game semantics model, revealing a new equation extending Church-style isomorphisms.
Contribution
It introduces a game semantics model for Curry-style system F and identifies a new type isomorphism equation specific to this setting.
Findings
Identifies a new type isomorphism equation for Curry-style system F.
Provides a game semantics framework combining syntax and semantics.
Extends the known equational system for Church-style to Curry-style types.
Abstract
Curry-style system F, ie. system F with no explicit types in terms, can be seen as a core presentation of polymorphism from the point of view of programming languages. This paper gives a characterisation of type isomorphisms for this language, by using a game model whose intuitions come both from the syntax and from the game semantics universe. The model is composed of: an untyped part to interpret terms, a notion of game to interpret types, and a typed part to express the fact that an untyped strategy plays on a game. By analysing isomorphisms in the model, we prove that the equational system corresponding to type isomorphisms for Curry-style system F is the extension of the equational system for Church-style isomorphisms with a new, non-trivial equation: forall X.A = A[forall Y.Y/X] if X appears only positively in A.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · semigroups and automata theory
