More Web Proxy on the site http://driver.im/

research-article

Open access

On polymorphic gradual typing

Authors:

Atsushi IgarashiAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 1, Issue ICFP

Article No.: 40, Pages 1 - 29

https://doi.org/10.1145/3110284

Published: 29 August 2017 Publication History

Abstract

We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guarantee—the so-called refined criteria, advocated by Siek et al. We develop System F_G, which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System F_C, which is based on previous polymorphic blame calculi by Ahmed et al. The design of System F_G and System F_C, geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System F_G satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.

Supplementary Material

Auxiliary Archive (icfp17-main50-s.zip)

This is a package of supplementary material and the paper artifact. The supplementary material (supplement.pdf) contains auxiliary definitions and proofs of the main theorems. The paper artifact, a VM image which contains System F_G interpreter implemented with OCaml, is "artifact/artifact.ova". You can find details of usage in "artifact/ArtifactOverview.txt" and the source code in "artifact/src/".

Download
2336.72 MB

References

[1]

Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. 1991. Dynamic Typing in a Statically Typed Language. 13, 2 (1991), 237–268.

[2]

Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Didier Rémy. 1995. Dynamic Typing in Polymorphic Languages. J. Funct. Program. 5, 1 (1995), 111–130.

[3]

Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler. 2009. Blame for all. In Proc. of Workshop on Stript to Program Evolution.

Digital Library

[4]

Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for all. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011. 201–214.

Digital Library

[5]

Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free: Parametricity, With and Without Types. Proc. ACM Program. Lang. 1, ICFP, Article 39 (sep 2017), 28 pages.

Digital Library

[6]

Amal Ahmed, James T. Perconti, Jeremy G. Siek, and Philip Wadler. 2013. Blame for All (revised). (2013).

[7]

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, Gothenburg, Sweden, September 1-3, 2014. 283–295.

Digital Library

[8]

João Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C. Pierce. 2011. Polymorphic Contracts. In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings. 18–37.

[9]

Gavin M. Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding TypeScript. In ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings. 257–281.

Digital Library

[10]

Gavin M. Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding Dynamic Types to C # . In ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings. 76–100.

[11]

Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt. 2016. Practical Optional Types for Clojure. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 68–94.

Digital Library

[12]

Luca Cardelli. 1986. A Polymorphic λ-calculus with Type:Type. Technical Report 10. DEC Systems Research Center.

[13]

Matteo Cimini and Jeremy G. Siek. 2016. The gradualizer: a methodology and algorithm for generating gradual type systems. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. 443–455.

Digital Library

[14]

Matteo Cimini and Jeremy G. Siek. 2017. Automatically generating the dynamic semantics of gradually typed languages. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 789–803.

Digital Library

[15]

Facebook. 2017. The Hack Programming Language. (2017). http://hacklang.org/.

[16]

Cormac Flanagan. 2006. Hybrid type checking. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006. 245–256.

Digital Library

[17]

Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 303–315.

Digital Library

[18]

Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting gradual typing. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 -22, 2016. 429–442.

Digital Library

[19]

Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse d’état. Université Paris VII. Summary in Proceedings of the Second Scandinavian Logic Symposium (J.E. Fenstad, editor), North-Holland, 1971 (pp. 63–92).

[20]

Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. 2010. Contracts made manifest. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. 353–364.

Digital Library

[21]

Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. 2006. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop.

[22]

Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. 2007. Relationally-parametric polymorphic contracts. In Proceedings of the 2007 Symposium on Dynamic Languages, DLS 2007, October 22, 2007, Montreal, Quebec, Canada. 29–40.

Digital Library

[23]

Lintaro Ina and Atsushi Igarashi. 2011. Gradual typing for generics. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22 - 27, 2011. 609–624.

Digital Library

[24]

Jacob Matthews and Amal Ahmed. 2008. Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!. In Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. 16–31.

[25]

Jacob Matthews and Robert Bruce Findler. 2009. Operational semantics for multi-language programs. ACM Trans. Program. Lang. Syst. 31, 3 (2009), 12:1–12:44.

Digital Library

[26]

Erik Meijer and Peter Drayton. 2004. Static Typing Where Possible, Dynamic Typing When Needed: The End of the Cold War Between Programming Languages. In OOPSLA’04 Workshop on Revival of Dynamic Languages.

[27]

James H. Morris, Jr. 1973. Protection in Programming Languages. 16, 1 (Jan. 1973), 15–21.

[28]

Georg Neis, Derek Dreyer, and Andreas Rossberg. 2011. Non-parametric parametricity. J. Funct. Program. 21, 4-5 (2011), 497–562.

Digital Library

[29]

Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Chapter 23.

[30]

John Reynolds. 1974. Towards a Theory of Type Structure. In Proc. Colloque sur la Programmation (Lecture Notes in Computer Science), Vol. 19. Springer-Verlag, 408–425.

[31]

Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg. 2017. Polymorphic Manifest Contracts, Revised and Resolved. ACM Trans. Program. Lang. Syst. 39, 1, Article 3 (Feb. 2017), 36 pages.

Digital Library

[32]

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

[33]

Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30 - August 3, 2007, Proceedings. 2–27.

Digital Library

[34]

Jeremy G. Siek and Manish Vachharajani. 2008. Gradual typing with unification-based inference. In Proceedings of the 2008 Symposium on Dynamic Languages, DLS 2008, July 8, 2008, Paphos, Cyprus. 7.

Digital Library

[35]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA. 274–293.

[36]

Jeremy G. Siek and Philip Wadler. 2010. Threesomes, with and without blame. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. 365–376.

Digital Library

[37]

Jeremy G. Siek and Philip Wadler. 2016. The key to blame: Gradual typing meets cryptography. (2016).

[38]

Satish Thatte. 1990. Quasi-static Typing. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1990. 367–381.

Digital Library

[39]

Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage migration: from scripts to programs. In Companion to the 21th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006, October 22-26, 2006, Portland, Oregon, USA. 964–974.

Digital Library

[40]

Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The design and implementation of typed scheme. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. 395–406.

Digital Library

[41]

Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. 2014. Design and Evaluation of Gradual Typing for Python. In Dynamic Language Symposium. 45–56.

Digital Library

[42]

Philip Wadler. 2015. A Complement to Blame. In 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA. 309–320.

[43]

Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. 1–16.

Digital Library

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
Gierczak OMenon LDimoulas CAhmed A(2024)Gradually Typed Languages Should Be Vigilant!Proceedings of the ACM on Programming Languages10.1145/36498428:OOPSLA1(864-892)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649842
SU CCHEN LYANHUI LZHOU Y(2024)Static Blame for gradual typingJournal of Functional Programming10.1017/S095679682400002934Online publication date: 25-Mar-2024
https://doi.org/10.1017/S0956796824000029
Show More Cited By

Index Terms

On polymorphic gradual typing
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
    2. General programming languages
      1. Language features
        Polymorphism
      2. Language types
        Functional languages

Recommendations

Gradual typing: a new perspective

We define a new, more semantic interpretation of gradual types and use it to ``gradualize'' two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define three gradual type ...
Dynamic type inference for gradual Hindley–Milner typing

Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. Soundness and completeness mean that, if the algorithm succeeds, ...
Gradual typing with union and intersection types

We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 1, Issue ICFP

September 2017

1173 pages

EISSN:2475-1421

DOI:10.1145/3136534

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 August 2017

Published in PACMPL Volume 1, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Japan Society for the Promotion of Science

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
1,105
Total Downloads

Downloads (Last 12 months)107
Downloads (Last 6 weeks)10

Reflects downloads up to 14 Dec 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
Gierczak OMenon LDimoulas CAhmed A(2024)Gradually Typed Languages Should Be Vigilant!Proceedings of the ACM on Programming Languages10.1145/36498428:OOPSLA1(864-892)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649842
SU CCHEN LYANHUI LZHOU Y(2024)Static Blame for gradual typingJournal of Functional Programming10.1017/S095679682400002934Online publication date: 25-Mar-2024
https://doi.org/10.1017/S0956796824000029
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
Malewski SGreenberg MTanter É(2021)Gradually structured dataProceedings of the ACM on Programming Languages10.1145/34855035:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485503
Fu WKrause FThiemann P(2021)Label dependent lambda calculus and gradual typingProceedings of the ACM on Programming Languages10.1145/34854855:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485485
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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