skip to main content
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
  • (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
  • (2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/357983345:1(1-54)Online publication date: 5-Mar-2023
  • (2022)Fifty Years of Prolog and BeyondTheory and Practice of Logic Programming10.1017/S147106842200010222:6(776-858)Online publication date: 17-May-2022
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

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

Qualifiers

  • Research-article

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
  • (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
  • (2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/357983345:1(1-54)Online publication date: 5-Mar-2023
  • (2022)Fifty Years of Prolog and BeyondTheory and Practice of Logic Programming10.1017/S147106842200010222:6(776-858)Online publication date: 17-May-2022
  • (2022)The StaDyn programming languageSoftwareX10.1016/j.softx.2022.10121120(101211)Online publication date: Dec-2022
  • (2020)Offload annotationsProceedings of the 2020 USENIX Conference on Usenix Annual Technical Conference10.5555/3489146.3489166(293-306)Online publication date: 15-Jul-2020
  • (2020)An Integrated Approach to Assertion-Based Random Testing in PrologLogic-Based Program Synthesis and Transformation10.1007/978-3-030-45260-5_10(159-176)Online publication date: 22-Apr-2020
  • (2019)Complete monitors for gradual typesProceedings of the ACM on Programming Languages10.1145/33605483:OOPSLA(1-29)Online publication date: 10-Oct-2019
  • (2019)Static TypeScript: an implementation of a static compiler for the TypeScript languageProceedings of the 16th ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes10.1145/3357390.3361032(105-116)Online publication date: 21-Oct-2019
  • (2019)Leveraging metamorphic testing to automatically detect inconsistencies in code generator familiesSoftware Testing, Verification and Reliability10.1002/stvr.172130:1Online publication date: 20-Dec-2019
  • (2016)Automatic non-functional testing of code generators familiesACM SIGPLAN Notices10.1145/3093335.299325652:3(202-212)Online publication date: 20-Oct-2016
  • 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