research-article

Open access

Graduality and parametricity: together again for the first time

Authors:

Amal AhmedAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue POPL

Article No.: 46, Pages 1 - 32

https://doi.org/10.1145/3371114

Published: 20 December 2019 Publication History

Abstract

Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are ``simply incompatible''. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work.

We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a language that satisfies both graduality and parametricity theorems. The language has a simple runtime semantics, which can be explained by translation to a statically typed language where the dynamic type is interpreted as a dynamically extensible sum type. Far from being in conflict, we show that the parametricity theorem follows as a direct corollary of a relational interpretation of the graduality property.

Supplementary Material

WEBM File (a46-new.webm)

Download
76.39 MB

References

[1]

Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-Dependent Representation Independence. In ACM Symposium on Principles of Programming Languages (POPL), Savannah, Georgia.

[2]

Amal Ahmed, Robert Bruce Findler, Jeremy Siek, and Philip Wadler. 2011. Blame for All. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas. 201–214.

[3]

Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free: Parametricity, With and Without Types. In International Conference on Functional Programming (ICFP), Oxford, United Kingdom.

[4]

Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A Theory of Gradual Effect Systems. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). 283–295.

Digital Library

[5]

John Boyland. 2014. The Problem of Structural Type Tests in a Gradually-Typed Language. In 21st Workshop on Foundations of Object-Oriented Languages.

[6]

Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. Proc. ACM Program. Lang. 1, ICFP, Article 41 (Aug. 2017), 28 pages.

Digital Library

[7]

Tim Disney and Cormac Flanagan. 2011. Gradual Information Flow Typing. In Workshop on Script-to-Program Evolution (STOP).

[8]

Brian Patrick Dunphy. 2002. Parametricity As a Notion of Uniformity in Reflexive Graphs. Ph.D. Dissertation. Champaign, IL, USA. Advisor(s) Reddy, Uday.

[9]

Matthias Felleisen. 1990. On the expressive power of programming languages. ESOP’90 (1990).

[10]

Luminous Fennell and Peter Thiemann. 2013. Gradual Security Typing with References. In CSF. IEEE Computer Society, 224–239.

[11]

Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs (POPL ’15).

[12]

Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In ACM Symposium on Principles of Programming Languages (POPL).

[13]

Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, and Philip Wadler. 2017b. Gradual Session Types. In International Conference on Functional Programming (ICFP).

[14]

Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017a. On Polymorphic Gradual Typing. In International Conference on Functional Programming (ICFP), Oxford, United Kingdom.

[15]

Lintaro Ina and Atsushi Igarashi. 2011. Gradual typing for generics. In Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications (OOPSLA ’11).

Digital Library

[16]

Nico Lehmann and Éric Tanter. 2017. Gradual Refinement Types. In ACM Symposium on Principles of Programming Languages (POPL).

[17]

Paul Blain Levy. 2003. Call-By-Push-Value: A Functional/Imperative Synthesis. Springer.

[18]

QingMing Ma and John C. Reynolds. 1991. Types, Abstractions, and Parametric Polymorphism, Part 2. In Mathematical Foundations of Programming Semantics, 7th International Conference, Pittsburgh, PA, USA.

[19]

John C. Mitchell and Gordon D. Plotkin. 1985. Abstract types have existential type. In ACM Symposium on Principles of Programming Languages (POPL), New Orleans, Louisiana.

[20]

Georg Neis, Derek Dreyer, and Andreas Rossberg. 2009. Non-Parametric Parametricity. In International Conference on Functional Programming (ICFP). 135–148.

[21]

Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs. In International Conference on Functional Programming (ICFP), St. Louis, Missouri.

[22]

Max S. New, Dustin Jamner, and Amal Ahmed. 2020. Technical Appendix to Graduality and Parametricity: Together Again for the First Time. http://www.ccs.neu.edu/home/amal/papers/gradparam- tr.pdf

[23]

Max S. New, Daniel R. Licata, and Amal Ahmed. 2019. Gradual Type Theory (POPL ’19).

[24]

Gordon Plotkin and Martín Abadi. 1993. A logic for parametric polymorphism. Typed Lambda Calculi and Applications (1993), 361–375.

[25]

John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France.

[26]

Amr Sabry and Matthias Felleisen. 1992. Reasoning about Programs in Continuation-Passing Style. In Conf. on LISP and functional programming, LFP ’92.

Digital Library

[27]

Ilya Sergey and Dave Clarke. 2012. Gradual Ownership Types. In ESOP (Lecture Notes in Computer Science), Vol. 7211. Springer, 579–599.

[28]

Jeremy Siek, Micahel Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages.

[29]

Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). 81–92.

[30]

Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In European Conference on Object-Oriented Programming (ECOOP).

Digital Library

[31]

Eijiro Sumii and Benjamin C. Pierce. 2004. A Bisimulation for Dynamic Sealing. In ACM Symposium on Principles of Programming Languages (POPL), Venice, Italy.

[32]

Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Gradual typing for first-class classes (ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA)).

[33]

Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage Migration: From Scripts to Programs. In Dynamic Languages Symposium (DLS). 964–974.

Digital Library

[34]

Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California.

[35]

Sam Tobin-Hochstadt, Vincent St-Amour, Eric Dobson, and Asumu Takikawa. [n. d.]. Typed Racket Reference. https: //docs.racket- lang.org/ts- reference/Typed_Units.html Accessed: 2019-10-30.

[36]

Matías Toro, Ronald Garcia, and Éric Tanter. 2018. Type-Driven Gradual Security with References. ACM Transactions on Programming Languages and Systems 40, 4 (Dec. 2018).

Digital Library

[37]

Matías Toro, Elizabeth Labrada, and Éric Tanter. 2019. Gradual Parametricity, Revisited. Proc. ACM Program. Lang. 3, POPL, Article 17 (Jan. 2019), 30 pages.

Digital Library

[38]

Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. 2011. Gradual Typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP’11).

Digital Library

[39]

Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent Subtyping for All. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 3–30.

Cited By

Igarashi AOzaki SSekiyama TTanabe Y(2024)Space-Efficient Polymorphic Gradual Typing, Mostly ParametricProceedings of the ACM on Programming Languages10.1145/36564418:PLDI(1585-1608)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656441
New MGiovannini ELicata D(2023)Gradual Typing for Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228607:OOPSLA2(1758-1786)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622860
Greenman B(2023)GTP Benchmarks for Gradual Typing PerformanceProceedings of the 2023 ACM Conference on Reproducibility and Replicability10.1145/3589806.3600034(102-114)Online publication date: 27-Jun-2023
https://dl.acm.org/doi/10.1145/3589806.3600034
Show More Cited By

Index Terms

Graduality and parametricity: together again for the first time
1. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Gradual type theory

Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based ...
Gradual parametricity, revisited

Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs were recently ...
Theorems for free for free: parametricity, with and without types

The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a ...

Comments

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
887
Total Downloads

Downloads (Last 12 months)109
Downloads (Last 6 weeks)15

Reflects downloads up to 21 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Igarashi AOzaki SSekiyama TTanabe Y(2024)Space-Efficient Polymorphic Gradual Typing, Mostly ParametricProceedings of the ACM on Programming Languages10.1145/36564418:PLDI(1585-1608)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656441
New MGiovannini ELicata D(2023)Gradual Typing for Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228607:OOPSLA2(1758-1786)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622860
Greenman B(2023)GTP Benchmarks for Gradual Typing PerformanceProceedings of the 2023 ACM Conference on Reproducibility and Replicability10.1145/3589806.3600034(102-114)Online publication date: 27-Jun-2023
https://dl.acm.org/doi/10.1145/3589806.3600034
Ye WOliveira B(2023)Pragmatic Gradual Polymorphism with ReferencesProgramming Languages and Systems10.1007/978-3-031-30044-8_6(140-167)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_6
Labrada EToro MTanter É(2022)Gradual System FJournal of the ACM10.1145/355598669:5(1-78)Online publication date: 28-Oct-2022
https://dl.acm.org/doi/10.1145/3555986
Devriese DPatrignani MPiessens F(2022)Two Parametricities Versus Three Universal TypesACM Transactions on Programming Languages and Systems10.1145/353965744:4(1-43)Online publication date: 21-Sep-2022
https://dl.acm.org/doi/10.1145/3539657
Labrada EToro MTanter ÉDevriese D(2022)Plausible sealing for gradual parametricityProceedings of the ACM on Programming Languages10.1145/35273146:OOPSLA1(1-28)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527314
Lennon-Bertrand MMaillard KTabareau NTanter É(2022)Gradualizing the Calculus of Inductive ConstructionsACM Transactions on Programming Languages and Systems10.1145/349552844:2(1-82)Online publication date: 6-Apr-2022
https://dl.acm.org/doi/10.1145/3495528
R KR DA A(2022)AI-Based Efficient WUGS Network Channel Modeling and Clustered Cooperative CommunicationACM Transactions on Sensor Networks10.1145/346903418:3(1-14)Online publication date: 18-Apr-2022
https://dl.acm.org/doi/10.1145/3469034
CAMPORA JCHEN SERWIG MWALKINGSHAW E(2022)Migrating gradual typesJournal of Functional Programming10.1017/S095679682200008932Online publication date: 6-Oct-2022
https://doi.org/10.1017/S0956796822000089
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents