The formal calculus System F models the essence of polymorphism and abstract data types, features that exist in many programming languages. The calculus’ core property is parametricity: a theorem expressing the language’s abstractions and validating important principles like information hiding and modularity.When System F is combined with features like recursive types, mutable state, continuations or exceptions, the formulation of parametricity needs to be adapted to follow suit, for example using techniques like step-indexing, Kripke world-indexing or biorthogonality. However, it is less clear how this formulation should change when System F is combined with untyped languages, gradual types, dynamic sealing and runtime type analysis (typecase) alongside type generation. Extensions of System F with these features have been proven to satisfy forms of parametricity (with Kripke worlds carrying semantic interpretations of types). However, the relative power of the modified formulations of parametricity with respect to others and the relative expressiveness of System F with and without these extensions are unknown.In this paper, we explain that the aforementioned different settings have a common characteristic: they do not enforce or preserve the lexical scope of System F’s type variables. Formally, this results in the existence of a universal type (note: this is not the same as a universally-quantified type). We explain why standard parametricity is incompatible with such a type and how type worlds resolve this. Building on these insights, we answer two open conjectures from the literature, negatively, and we point out a deficiency in current proposals for combining System F with gradual types.

Two Parametricities Versus Three Universal Types / Devriese, Dominique; Patrignani, Marco; Piessens, Frank. - In: ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS. - ISSN 0164-0925. - 44:4(2022), pp. 2301-2343. [10.1145/3539657]

Two Parametricities Versus Three Universal Types

Marco Patrignani;
2022-01-01

Abstract

The formal calculus System F models the essence of polymorphism and abstract data types, features that exist in many programming languages. The calculus’ core property is parametricity: a theorem expressing the language’s abstractions and validating important principles like information hiding and modularity.When System F is combined with features like recursive types, mutable state, continuations or exceptions, the formulation of parametricity needs to be adapted to follow suit, for example using techniques like step-indexing, Kripke world-indexing or biorthogonality. However, it is less clear how this formulation should change when System F is combined with untyped languages, gradual types, dynamic sealing and runtime type analysis (typecase) alongside type generation. Extensions of System F with these features have been proven to satisfy forms of parametricity (with Kripke worlds carrying semantic interpretations of types). However, the relative power of the modified formulations of parametricity with respect to others and the relative expressiveness of System F with and without these extensions are unknown.In this paper, we explain that the aforementioned different settings have a common characteristic: they do not enforce or preserve the lexical scope of System F’s type variables. Formally, this results in the existence of a universal type (note: this is not the same as a universally-quantified type). We explain why standard parametricity is incompatible with such a type and how type worlds resolve this. Building on these insights, we answer two open conjectures from the literature, negatively, and we point out a deficiency in current proposals for combining System F with gradual types.
2022
4
Devriese, Dominique; Patrignani, Marco; Piessens, Frank
Two Parametricities Versus Three Universal Types / Devriese, Dominique; Patrignani, Marco; Piessens, Frank. - In: ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS. - ISSN 0164-0925. - 44:4(2022), pp. 2301-2343. [10.1145/3539657]
File in questo prodotto:
File Dimensione Formato  
poly-seal-no-j.pdf

accesso aperto

Descrizione: paper pdf
Tipologia: Pre-print non referato (Non-refereed preprint)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 923.34 kB
Formato Adobe PDF
923.34 kB Adobe PDF Visualizza/Apri
3539657.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 1.03 MB
Formato Adobe PDF
1.03 MB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/362402
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact