skip to main content
10.1145/2676726.2676971acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Safe & Efficient Gradual Typing for TypeScript

Published: 14 January 2015 Publication History

Abstract

Current proposals for adding gradual typing to JavaScript, such as Closure, TypeScript and Dart, forgo soundness to deal with issues of scale, code reuse, and popular programming patterns. We show how to address these issues in practice while retaining soundness. We design and implement a new gradual type system, prototyped for expediency as a 'Safe' compilation mode for TypeScript. Our compiler achieves soundness by enforcing stricter static checks and embedding residual runtime checks in compiled code. It emits plain JavaScript that runs on stock virtual machines. Our main theorem is a simulation that ensures that the checks introduced by Safe TypeScript (1) catch any dynamic type error, and (2) do not alter the semantics of type-safe TypeScript code.
Safe TypeScript is carefully designed to minimize the performance overhead of runtime checks. At its core, we rely on two new ideas: differential subtyping, a new form of coercive subtyping that computes the minimum amount of runtime type information that must be added to each object; and an erasure modality, which we use to safely and selectively erase type information. This allows us to scale our design to full-fledged TypeScript, including arrays, maps, classes, inheritance, overloading, and generic types.
We validate the usability and performance of Safe TypeScript empirically by type-checking and compiling around 120,000 lines of existing TypeScript source code. Although runtime checks can be expensive, the end-to-end overhead is small for code bases that already have type annotations. For instance, we bootstrap the Safe TypeScript compiler (90,000 lines including the base TypeScript compiler): we measure a 15% runtime overhead for type safety, and also uncover programming errors as type safety violations. We conclude that, at least during development and testing, subjecting JavaScript/TypeScript programs to safe gradual typing adds significant value to source type annotations at a modest cost.

Supplementary Material

MOV File (2676971.mov)

References

[1]
M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. In Proceedings of POPL, 1989.
[2]
A. Ahmed, R. B. Findler, J. G. Siek, and P. Wadler. Blame for all. In Proceedings of POPL, 2011.
[3]
E. Allende, J. Fabry, and É. Tanter. Cast insertion strategies for gradually-typed objects. In Proceedings of DLS, 2013.
[4]
E. Allende, J. Fabry, R. Garcia, and É. Tanter. Confined gradual typing. In Proceedings of OOPSLA, 2014.
[5]
C. Anderson, P. Giannini, and S. Drossopoulou. Towards type inference for JavaScript. In Proceedings of ECOOP, 2005.
[6]
G. Bierman, M. Abadi, and M. Torgersen. Understanding TypeScript. In Proceedings of ECOOP, 2014.
[7]
R. Cartwright and M. Fagan. Soft typing. In Proceedings of PLDI, 1991.
[8]
R. Chugh, D. Herman, and R. Jhala. Dependent types for JavaScript. In Proceedings of OOSLA, 2012.
[9]
M. Fagan. Soft Typing: An Approach to Type Checking for Dynamically Typed Languages. PhD thesis, 1990.
[10]
A. Feldthaus and A. Müller. Checking correctness of TypeScript interfaces for JavaScript libraries. In Proceedings of OOPSLA, 2014.
[11]
A. Guha, C. Saftoiu, and S. Krishnamurthi. The essence of JavaScript. In Proceedings of ECOOP, 2010.
[12]
A. Guha, C. Saftoiu, and S. Krisnamurthi. Typing local control and state using flow analysis. In Proceedings of ESOP, 2011.
[13]
F. Henglein and J. Rehof. Safe polymorphic type inference for Scheme: Translating Scheme to ML. In Proceedings of FPCA, 1995.
[14]
D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. Higher Order Symbol. Comput., 2010.
[15]
B. S. Lerner, J. G. Politz, A. Guha, and S. Krishnamurthi. TeJaS: Retrofitting type systems for JavaScript. In Proceedings of DLS, 2013.
[16]
Z. Luo. Coercive subtyping. J. Log. Comput., 9 (1): 105--130, 1999.
[17]
M. S. Miller, M. Samuel, B. Laurie, I. Awad, and M. Stay. Caja: Safe active content in sanitized JavaScript. Unpublished paper, 2007.
[18]
A. Rastogi, N. Swamy, C. Fournet, G. Bierman, and P. Vekris. Safe & efficient gradual typing for TypeScript, MSR-TR-2014--99, 2014.
[19]
G. Richards, F. Z. Nardelli, C. Rouleau, and J. Vitek. Types you can count on. Unpublished paper, 2014.
[20]
J. G. Siek and W. Taha. Gradual typing for functional languages. In Proceedings of Scheme and functional programming workshop, 2006.
[21]
J. G. Siek and W. Taha. Gradual typing for objects. In Proceedings of ECOOP, 2007.
[22]
J. G. Siek and M. M. Vitousek. Monotonic references for gradual typing. Unpublished paper, 2013.
[23]
N. Swamy, J. Weinberger, C. Schlesinger, J. Chen, and B. Livshits. Verifying higher-order programs with the Dijkstra monad. In Proceedings of PLDI, 2013.
[24]
N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen, P.-Y. Strub, and G. Bierman. Gradual typing embedded securely in JavaScript. In Proceedings of POPL, 2014.
[25]
A. Takikawa, T. S. Stickland, C. Dimoulas, S. Tobin-Hochstadt, and M. Felleisen. Gradual typing for first-class classes. In Proceedings of OOPSLA, 2012.
[26]
P. Thiemann. Towards a type systems for analyzing JavaScript programs. In Proceedings of ESOP, 2005.
[27]
N. Tillmann, M. Moskal, J. de Halleux, M. Fähndrich, and S. Burckhardt. Touchdevelop: app development on mobile devices. In Proceedings of FSE, 2012.
[28]
S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: from scripts to programs. In Proceedings of DLS, 2006.
[29]
S. Tobin-Hochstadt and M. Felleisen. The design and implementation of Typed Scheme. In Proceedings of POPL, 2008.
[30]
J. Turner. Announcing TypeScript 1.1 CTP, 2014. http://blogs.msdn.com/b/typescript/archive/2014/10/06/announcing-typescript-1--1-ctp.aspx.
[31]
M. M. Vitousek, A. M. Kent, J. G. Siek, and J. Baker. Design and evaluation of gradual typing for Python. In Proceedings of DLS, 2014.
[32]
P. Wadler and R. B. Findler. Well-typed programs can't be blamed. In Proceedings of ESOP, 2009.
[33]
A. K. Wright and R. Cartwright. A practical soft type system for scheme. ACM Trans. Program. Lang. Syst., 19 (1): 87--152, Jan. 1997. 10.1145/239912.239917.
[34]
lund, and Vitek}ThornT. Wrigstad, F. Z. Nardelli, S. Lebresne, J. Östlund, and J. Vitek. Integrating typed and untyped code in a scripting language. In Proceedings of POPL, 2010.

Cited By

View all
  • (2024)Typed and Confused: Studying the Unexpected Dangers of Gradual TypingProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695549(1858-1870)Online publication date: 27-Oct-2024
  • (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
  • (2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
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].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. gradual typing
  2. javascript
  3. type safety
  4. typescript

Qualifiers

  • Research-article

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)126
  • Downloads (Last 6 weeks)10
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Typed and Confused: Studying the Unexpected Dangers of Gradual TypingProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695549(1858-1870)Online publication date: 27-Oct-2024
  • (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
  • (2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
  • (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: 14-Jul-2024
  • (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
  • (2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/357983345:1(1-54)Online publication date: 5-Mar-2023
  • (2023)Learning to Predict User-Defined TypesIEEE Transactions on Software Engineering10.1109/TSE.2022.317894549:4(1508-1522)Online publication date: 1-Apr-2023
  • (2023)TypeScript’s Evolution: An Analysis of Feature Adoption Over Time2023 IEEE/ACM 20th International Conference on Mining Software Repositories (MSR)10.1109/MSR59073.2023.00027(109-114)Online publication date: May-2023
  • (2023)Enhancing embedded systems development with TSAutomated Software Engineering10.1007/s10515-023-00404-x31:1Online publication date: 6-Dec-2023
  • (2023)What Types Are Needed for Typing Dynamic Objects? A Python-Based Empirical StudyProgramming Languages and Systems10.1007/978-981-99-8311-7_2(24-45)Online publication date: 21-Nov-2023
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media