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

research-article

Open access

Transitioning from structural to nominal code with efficient gradual typing

Authors:

Fabian Muehlboeck,

Ross TateAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue OOPSLA

Article No.: 127, Pages 1 - 29

https://doi.org/10.1145/3485504

Published: 15 October 2021 Publication History

Abstract

Gradual typing is a principled means for mixing typed and untyped code. But typed and untyped code often exhibit different programming patterns. There is already substantial research investigating gradually giving types to code exhibiting typical untyped patterns, and some research investigating gradually removing types from code exhibiting typical typed patterns. This paper investigates how to extend these established gradual-typing concepts to give formal guarantees not only about how to change types as code evolves but also about how to change such programming patterns as well.

In particular, we explore mixing untyped "structural" code with typed "nominal" code in an object-oriented language. But whereas previous work only allowed "nominal" objects to be treated as "structural" objects, we also allow "structural" objects to dynamically acquire certain nominal types, namely interfaces. We present a calculus that supports such "cross-paradigm" code migration and interoperation in a manner satisfying both the static and dynamic gradual guarantees, and demonstrate that the calculus can be implemented efficiently.

Supplementary Material

Auxiliary Presentation Video (oopsla21main-p130-p-video.mp4)

This is a presentation video of our talk at OOPSLA 2021, describing the contributions of our paper, "Transitioning from Structural to Nominal Code with Efficient Gradual Typing", in particular, our extension of gradual reasoning to migrating between coding paradigms, and some design details of the language MonNom, which we co-designed to offer this additional migration path while both satisfying the gradual guarantees and allowing an efficient implementation.

Download
99.96 MB

References

[1]

Bowen Alpern, Anthony Cocchi, Stephen Fink, and David Grove. 2001. Efficient Implementation of Java Interfaces: Invokeinterface Considered Harmless. In OOPSLA. ACM, New York, NY, USA, 108–124.

Digital Library

[2]

Christopher Anderson and Sophia Drossopoulou. 2003. BabyJ: From Object Based to Class Based Programming via Types. Electronic Notes in Theoretical Computer Science 82, 8 (2003), 53–81. WOOD.

[3]

Spenser Bauman, Carl Friedrich Bolz-Tereick, Jeremy Siek, and Sam Tobin-Hochstadt. 2017. Sound Gradual Typing: Only Mostly Dead. PACMPL 1, OOPSLA, Article 54 (2017), 24 pages.

Digital Library

[4]

Gavin Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding Dynamic Types to C#. In ECOOP. Springer Berlin Heidelberg, Berlin, Heidelberg, 76–100.

[5]

John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw. 2017. Migrating Gradual Types. PACMPL 2, POPL, Article 15 (2017), 29 pages.

Digital Library

[6]

Craig Chambers, David Ungar, and Elgin Lee. 1989. An Efficient Implementation of SELF, a Dynamically-Typed Object-Oriented Language Based on Prototypes. In OOPSLA. Association for Computing Machinery, New York, NY, USA, 49–70.

Digital Library

[7]

Daniel Feltey, Ben Greenman, Christophe Scholliers, Robert Bruce Findler, and Vincent St-Amour. 2018. Collapsible Contracts: Fixing a Pathology of Gradual Typing. PACMPL 2, OOPSLA, Article 133 (2018), 27 pages.

Digital Library

[8]

Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In POPL. ACM, New York, NY, USA, 429–442.

Digital Library

[9]

Ben Greenman and Matthias Felleisen. 2018. A Spectrum of Type Soundness and Performance. PACMPL 2, ICFP, Article 71 (2018), 32 pages.

Digital Library

[10]

Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. 2006. Sage: Hybrid Checking for Flexible Specifications. Scheme and Functional Programming Workshop 6 (2006), 93–104. http://scheme2006.cs.uchicago.edu/06-freund.pdf

[11]

David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Space-Efficient Gradual Typing. Higher Order Symbol. Comput. 23, 2 (2010), 167–189.

Digital Library

[12]

Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G Siek. 2018. An Efficient Compiler for the Gradually Typed Lambda Calculus. Scheme and Functional Programming Workshop 18 (2018), 19 pages. http://www.schemeworkshop.org/2018/Kuhlenschmidt_Almahallawi_Siek.pdf

[13]

Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G. Siek. 2019. Toward Efficient Gradual Typing for Structural Types via Coercions. In PLDI. ACM, New York, NY, USA, 517–532.

Digital Library

[14]

Barbara H. Liskov and Jeannette M. Wing. 1994. A Behavioral Notion of Subtyping. ACM Trans. Program. Lang. Syst. 16, 6 (Nov. 1994), 1811–1841. issn:0164-0925

Digital Library

[15]

Jacob Matthews and Robert Bruce Findler. 2007. Operational Semantics for Multi-Language Programs. In POPL. Association for Computing Machinery, New York, NY, USA, 3–10.

Digital Library

[16]

Cameron Moy, Phúc C. Nguy ên, Sam Tobin-Hochstadt, and David Van Horn. 2021. Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification. PACMPL 5, POPL, Article 53 (2021), 28 pages.

Digital Library

[17]

Fabian Muehlboeck and Ross Tate. 2017. Sound Gradual Typing is Nominally Alive and Well. PACMPL 1, OOPSLA, Article 56 (2017), 30 pages.

Digital Library

[18]

Fabian Muehlboeck and Ross Tate. 2021. Transitioning from Structural to Nominal Code with Efficient Gradual Typing: Artifact.

Digital Library

[19]

Fabian Muehlboeck and Ross Tate. 2021. Transitioning from Structural to Nominal Code with Efficient Gradual Typing: Technical Report. https://www.cs.cornell.edu/~ross/publications/monnom/

[20]

Max S. New, Daniel R. Licata, and Amal Ahmed. 2019. Gradual Type Theory. PACMPL 3, POPL, Article 15 (2019), 31 pages.

Digital Library

[21]

Gregor Richards, Ellen Arteca, and Alexi Turcotte. 2017. The VM Already Knew That: Leveraging Compile-Time Knowledge to Optimize Gradual Typing. PACMPL 1, OOPSLA, Article 55 (2017), 27 pages.

Digital Library

[22]

Richard Roberts, Stefan Marr, Michael Homer, and James Noble. 2019. Transient Typechecks Are (Almost) Free. In ECOOP. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, Article 5, 28 pages.

[23]

Jeremy Siek and Walid Taha. 2007. Gradual Typing for Objects. In ECOOP. Springer Berlin Heidelberg, Berlin, Heidelberg, 2–27.

Digital Library

[24]

Jeremy G Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. Scheme and Functional Programming Workshop 6 (2006), 81–92. http://scheme2006.cs.uchicago.edu/13-siek.pdf

[25]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In SNAPL. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 274–293.

[26]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. 2015. Monotonic References for Efficient Gradual Typing. In ESOP. Springer Berlin Heidelberg, Berlin, Heidelberg, 432–456.

Digital Library

[27]

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. 2016. Is Sound Gradual Typing Dead?. In POPL. ACM, New York, NY, USA, 456–468.

Digital Library

[28]

Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage Migration: From Scripts to Programs. In OOPSLA. ACM, New York, NY, USA, 964–974.

Digital Library

[29]

Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. 2017. Migratory Typing: Ten Years Later. In SNAPL. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, Article 17, 17 pages.

[30]

Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. 2014. Design and Evaluation of Gradual Typing for Python. In DLS. ACM, New York, NY, USA, 45–56.

Digital Library

[31]

Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. 2017. Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems. In POPL. ACM, New York, NY, USA, 762–774.

Digital Library

[32]

Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek. 2010. Integrating Typed and Untyped Code in a Scripting Language. In POPL. ACM, New York, NY, USA, 377–388.

Digital Library

Cited By

Ye WOliveira BToro M(2024)Merging Gradual TypingProceedings of the ACM on Programming Languages10.1145/36897348:OOPSLA2(648-676)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689734
Greenman BFelleisen MDimoulas C(2023)How Profilers Can Help Navigate Type MigrationProceedings of the ACM on Programming Languages10.1145/36228177:OOPSLA2(544-573)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622817

Index Terms

Transitioning from structural to nominal code with efficient gradual typing
1. General and reference
  1. Cross-computing tools and techniques
    1. Performance
2. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
    2. General programming languages
      1. Language types
        Multiparadigm languages
        Object oriented languages
  2. Software organization and properties
    1. Extra-functional properties
      1. Interoperability

Recommendations

Sound gradual typing is nominally alive and well

Recent research has identified significant performance hurdles that sound gradual typing needs to overcome. These performance hurdles stem from the fact that the run-time checks gradual type systems insert into code can cause significant overhead. We ...
On polymorphic gradual typing

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 ...
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, ...

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 5, Issue OOPSLA

October 2021

2001 pages

EISSN:2475-1421

DOI:10.1145/3492349

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 October 2021

Published in PACMPL Volume 5, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
307
Total Downloads

Downloads (Last 12 months)117
Downloads (Last 6 weeks)20

Reflects downloads up to 23 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ye WOliveira BToro M(2024)Merging Gradual TypingProceedings of the ACM on Programming Languages10.1145/36897348:OOPSLA2(648-676)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689734
Greenman BFelleisen MDimoulas C(2023)How Profilers Can Help Navigate Type MigrationProceedings of the ACM on Programming Languages10.1145/36228177:OOPSLA2(544-573)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622817

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