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

research-article

Public Access

Big types in little runtime: open-world soundness and collaborative blame for gradual type systems

Authors:

Michael M. Vitousek,

Cameron Swords,

Jeremy G. SiekAuthors Info & Claims

ACM SIGPLAN Notices, Volume 52, Issue 1

Pages 762 - 774

https://doi.org/10.1145/3093333.3009849

Published: 01 January 2017 Publication History

Abstract

Gradual typing combines static and dynamic typing in the same language, offering programmers the error detection and strong guarantees of static types and the rapid prototyping and flexible programming idioms of dynamic types. Many gradually typed languages are implemented by translation into an untyped target language (e.g., Typed Clojure, TypeScript, Gradualtalk, and Reticulated Python). For such languages, it is desirable to support arbitrary interaction between translated code and legacy code in the untyped language while maintaining the type soundness of the translated code. In this paper we formalize this goal in the form of the open-world soundness criterion. We discuss why it is challenging to achieve open-world soundness using the traditional proxy-based approach for higher-order casts. However, the transient design satisfies open-world soundness. Indeed, we present a formal semantics for the transient design and prove that our semantics satisfies open-world soundness. In this paper we also solve a challenging problem for the transient design: how to provide blame tracking without proxies. We define a semantics for blame and prove the Blame Theorem. We also prove that the Gradual Guarantee holds for this system, ensuring that programs can be evolved freely between static and dynamic typing. Finally, we demonstrate that the runtime overhead of the transient approach is low in the context of Reticulated Python, an implementation of gradual typing for Python.

References

[1]

M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. In POPL, 1989.

Digital Library

[2]

Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for all. In POPL, 2011.

Digital Library

[3]

Esteban Allende, Oscar Calla´u, Johan Fabry, Éric Tanter, and Markus Denker. Gradual typing for smalltalk. Science of Computer Programming, August 2013.

Digital Library

[4]

Esteban Allende, Johan Fabry, and Éric Tanter. Cast insertion strategies for gradually-typed objects. In DLS, 2013.

Digital Library

[5]

Christopher Anderson and Sophia Drossopoulou. BabyJ - from object based to class based programming via types. In Workshop on Object Oriented Developments, 2003.

[6]

Andrew W. Appel. Compiling with Continuations. Cambridge University Press, New York, NY, USA, 2007.

Digital Library

[7]

Gavin Bierman, Erik Meijer, and Mads Torgersen. In ECOOP. Springer-Verlag.

[8]

Bard Bloom, John Field, Nathaniel Nystrom, Johan Östlund, Gregor Richards, Rok Strniˇsa, Jan Vitek, and Tobias Wrigstad. Thorn: Robust, concurrent, extensible scripting on the jvm. In OOPSLA, 2009.

Digital Library

[9]

Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstad. Practical optional types for clojure. In ESOP, 2016.

[10]

Gilad Bracha and David Griswold. Strongtalk: Typechecking smalltalk in a production environment. In OOPSLA, New York, NY, USA, 1993. ACM.

Digital Library

[11]

Robert Cartwright. User-defined data types as an aid to verifying LISP programs. In ICALP, 1976.

[12]

Craig Chambers and the Cecil Group. The Cecil language: Specification and rationale. Technical report, Department of Computer Science and Engineering, University of Washington, Seattle, Washington, 2004.

[13]

Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, and Matthias Felleisen. Correct blame for contracts: no more scapegoating. In POPL, 2011.

Digital Library

[14]

Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Complete monitors for behavioral contracts. In ESOP, 2012.

Digital Library

[15]

Eiffel. The Power of Design by Contract.

[16]

Facebook. Hack, 2013.

[17]

Robert Bruce Findler and Matthias Blume. Contracts as pairs of projections. In FLOPS, 2006.

Digital Library

[18]

Robert Bruce Findler and Matthias Felleisen. Contracts for higherorder functions. In ICFP, 2002.

Digital Library

[19]

Cormac Flanagan. Hybrid type checking. In POPL, Charleston, South Carolina, 2006.

Digital Library

[20]

Google. Dart: structured web apps, 2011.

[21]

Kathryn E. Gray, Robert Bruce Findler, and Matthew Flatt. Finegrained interoperability through mirrors and contracts. In OOPSLA. ACM Press, 2005.

Digital Library

[22]

Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, New York, NY, USA, 2012.

Digital Library

[23]

David Herman, Aaron Tomb, and Cormac Flanagan. Space-efficient gradual typing. In Trends in Functional Programming, 2007.

[24]

Matthias Keil and Peter Thiemann. Blame assignment for higher-order contracts with intersection and union. In ICFP, 2015.

Digital Library

[25]

Matthias Keil and Peter Thiemann. Transparent object proxies in JavaScript. In ECOOP, 2015.

[26]

Gianluca Mezzetti, Anders Møller, and Fabio Strocco. Type unsoundness in practice: An empirical study of Dart. In DLS, 2016.

Digital Library

[27]

Microsoft. Typescript, 2012.

[28]

Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. The ins and outs of gradual type inference. In POPL, 2012.

Digital Library

[29]

Aseem Rastogi, Nikhil Swamy, Cedric Fournet, Gavin Bierman, and Panagiotis Vekris. Safe & efficient gradual typing for TypeScript. Technical Report MSR-TR-2014-99, Microsoft Research, 2014.

[30]

Brianna M. Ren, John Toman, T. Stephen Strickland, and Jeffrey S. Foster. The ruby type checker. In Symposium on Applied Computing, 2013.

Digital Library

[31]

Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete Types for TypeScript. In ECOOP, 2015.

[32]

Manuel Serrano. Bigloo: a practical Scheme compiler. Inria-Rocquencourt, April 2002.

[33]

Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006.

[34]

Jeremy G. Siek and Philip Wadler. Threesomes, with and without blame. In POPL, 2010.

Digital Library

[35]

Jeremy G. Siek, Ronald Garcia, and Walid Taha. Exploring the design space of higher-order casts. In ESOP, 2009.

Digital Library

[36]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In SNAPL ’15, 2015.

[37]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. Monotonic references for efficient gradual typing. In ESOP, 2015.

Digital Library

[38]

T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. Chaperones and impersonators: run-time support for reasonable interposition. In OOPSLA, 2012.

Digital Library

[39]

Nikhil Swamy, Cedric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin Bierman. Gradual typing embedded securely in javascript. In POPL, 2014.

Digital Library

[40]

Cameron Swords, Amr Sabry, and Sam Tobin-Hochstadt. Expressing contract monitors as patterns of communication. In ICFP, 2015.

Digital Library

[41]

Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Gradual typing for firstclass classes. In OOPSLA, 2012.

Digital Library

[42]

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. Is sound gradual typing dead? In POPL, 2016.

Digital Library

[43]

Satish Thatte. Quasi-static typing. In POPL, 1990.

Digital Library

[44]

Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: From scripts to programs. In DLS, 2006.

[45]

Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of Typed Scheme. In POPL, January 2008.

Digital Library

[46]

Sam Tobin-Hochstadt and Matthias Felleisen. Logical types for untyped languages. In ICFP, 2010.

Digital Library

[47]

Michael M. Vitousek and Jeremy G. Siek. Gradual typing in an open world. Technical Report TR729, Indiana University, 2016.

[48]

Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. Design and evaluation of gradual typing for Python. In DLS, 2014.

Digital Library

[49]

Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. Big types in little runtime: Supplemental material, January 2017.

[50]

Philip Wadler and Robert Bruce Findler. Well-typed programs can’t be blamed. In ESOP, 2009.

Digital Library

[51]

Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994. ISSN 0890-5401.

Digital Library

[52]

Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek. In POPL, 2010.

Cited By

Greenman BDimoulas CFelleisen M(2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/3579833Online publication date: 12-Jan-2023
https://doi.org/10.1145/3579833
Wadler P(2021)GATE: Gradual Effect TypesLeveraging Applications of Formal Methods, Verification and Validation10.1007/978-3-030-89159-6_21(335-345)Online publication date: 12-Oct-2021
https://doi.org/10.1007/978-3-030-89159-6_21
Eremondi JTanter ÉGarcia R(2019)Approximate normalization for gradual dependent typesProceedings of the ACM on Programming Languages10.1145/33416923:ICFP(1-30)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341692
Show More Cited By

Index Terms

Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

Toward efficient gradual typing for structural types via coercions
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Gradual typing combines static and dynamic typing in the same program. Siek et al. (2015) describe five criteria for gradually typed languages, including type soundness and the gradual guarantee. A significant number of languages have been developed in ...
Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Gradual typing combines static and dynamic typing in the same language, offering programmers the error detection and strong guarantees of static types and the rapid prototyping and flexible programming idioms of dynamic types. Many gradually typed ...
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 ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 52, Issue 1

POPL '17

January 2017

901 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3093333

Editor:
Matthew Fluet

Issue’s Table of Contents

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2017
901 pages
ISBN:9781450346603
DOI:10.1145/3009837
General Chair:
Giuseppe Castagna
Paris Diderot University, France / CNRS, France
,
Program Chair:
Andrew D. Gordon
Microsoft Research, UK / University of Edinburgh, UK

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2017

Published in SIGPLAN Volume 52, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
1,239
Total Downloads

Downloads (Last 12 months)250
Downloads (Last 6 weeks)24

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Greenman BDimoulas CFelleisen M(2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/3579833Online publication date: 12-Jan-2023
https://doi.org/10.1145/3579833
Wadler P(2021)GATE: Gradual Effect TypesLeveraging Applications of Formal Methods, Verification and Validation10.1007/978-3-030-89159-6_21(335-345)Online publication date: 12-Oct-2021
https://doi.org/10.1007/978-3-030-89159-6_21
Eremondi JTanter ÉGarcia R(2019)Approximate normalization for gradual dependent typesProceedings of the ACM on Programming Languages10.1145/33416923:ICFP(1-30)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341692
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
Campora JKhan MChen S(2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632931
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
Khan MChen S(2024)Gradual Typing Performance, Micro Configurations and Macro PerspectivesTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_15(261-278)Online publication date: 29-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64626-3_15
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
Lazarek LGreenman BFelleisen MDimoulas C(2023)How to Evaluate Blame for Gradual Types, Part 2Proceedings of the ACM on Programming Languages10.1145/36078367:ICFP(159-186)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607836
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

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 Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents