Gradual Parametricity, Revisited
| Autor: | Matías Toro, Éric Tanter, Elizabeth Labrada |
|---|---|
| Přispěvatelé: | Department of Computer Science [Santiago, Chile] (DCC), Universidad de Chile = University of Chile [Santiago] (UCHILE), Programming securely with cryptography (PROSECCO ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), European Project: 715753,H2020,SECOMP(2017), Programming securely with cryptography (PROSECCO) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Parametric polymorphism
Conjecture [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Computer science Programming language System F 020207 software engineering Gradual typing 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences 010201 computation theory & mathematics Metatheory 0202 electrical engineering electronic engineering information engineering Parametricity Reference implementation Safety Risk Reliability and Quality computer Software Parametric statistics |
| Zdroj: | Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (POPL), ⟨10.1145/3290330⟩ Proceedings of the ACM on Programming Languages, 2019, 3 (POPL), ⟨10.1145/3290330⟩ |
| ISSN: | 2475-1421 |
| DOI: | 10.1145/3290330⟩ |
| Popis: | International audience; Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, whilepreserving relational parametricity, has proven extremely challenging: first attempts were formulated a decadeago, and several recent developments have been published in the past year. In addition to leaving someproperties as conjectures or future work, we observe that all prior work improperly handle type instantiationswhen imprecise types are involved. This observation further suggests that existing polymorphic cast calculiare not well suited for supporting a gradual counterpart of System F. Consequently, we revisit the challengeof designing a gradual language with explicit parametric polymorphism, exploring the extent to which theAbstracting Gradual Typing methodology helps us derive such a language, GSF. We present the design andmetatheory of GSF, and provide a reference implementation. In addition to avoiding the uncovered semanticissues, GSF satisfies all the expected properties of a gradual parametric language, save for one property:the dynamic gradual guarantee, which was left as conjecture in all prior work, is here proven to be simplyincompatible with parametricity. We nevertheless establish a weaker property that allows us to disprove severalclaims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricity |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|