research-article

Type inference for static compilation of JavaScript

Authors:

Satish Chandra,

Colin S. Gordon,

Jean-Baptiste Jeannin,

Cole Schlesinger,

Manu Sridharan,

Youngil ChoiAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 10

Pages 410 - 429

https://doi.org/10.1145/3022671.2984017

Published: 19 October 2016 Publication History

Abstract

We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive enough to accommodate several standard benchmarks with only minor workarounds. The invariants enforced by the types enable an ahead-of-time compiler to carry out optimizations typically beyond the reach of static compilers for dynamic languages. Unlike previous inference techniques for prototype inheritance, our algorithm uses a combination of lower and upper bound propagation to infer types and discover type errors in all code, including uninvoked functions. The inference is expressed in a simple constraint language, designed to leverage off-the-shelf fixed point solvers. We prove soundness for both the type system and inference algorithm. An experimental evaluation showed that the inference is powerful, handling the aforementioned benchmarks with no manual type annotation, and that the inferred types enable effective static compilation.

Supplementary Material

Auxiliary Archive (p410-chandra-s.zip)

This archive contains the benchmarks listed in Table 2 of the paper, ported to our JavaScript subset.

Download
35.39 KB

References

[1]

Octane Benchmarks. https://developers.google.com/ octane/.

[2]

SunSpider Benchmarks. https://www.webkit.org/perf/ sunspider/sunspider.html.

[3]

Flow. http://www.flowtype.org.

[4]

JetStream Benchmarks. http://browserbench.org/ JetStream/.

[5]

JavaScriptCore JavaScript engine. http://trac.webkit. org/wiki/JavaScriptCore.

[6]

The Redmonk Programming Language Rankings: June 2015.

[7]

https://redmonk.com/sogrady/2015/07/01/ language-rankings-6-15/.

[8]

Tizen Platform. https://www.tizen.org/.

[9]

TypeScript. http://www.typescriptlang.org.

[10]

V8 JavaScript Engine. https://developers.google.com/ v8/.

[11]

T.J. Watson Libraries for Analysis (WALA). http://wala. sf.net, 2015.

[12]

Martín Abadi and Luca Cardelli. A Theory of Primitive Objects: Untyped and First-order Systems. Information and Computation, 125(2):78–102, 1996.

Digital Library

[13]

Ole Agesen, Jens Palsberg, and Michael I. Schwartzbach. Type Inference of SELF. In Proceedings of the 7th European Conference on Object-Oriented Programming, ECOOP ’93, pages 247–267, London, UK, UK, 1993. Springer-Verlag.

Digital Library

[14]

ISBN 3-540-57120-5.

[15]

Alexander Aiken. Introduction to Set Constraint-based Program Analysis. Sci. Comput. Program., November 1999. ISSN 0167-6423.

Digital Library

[16]

Christopher Anderson, Paola Giannini, and Sophia Drossopoulou. Towards Type Inference for JavaScript. In ECOOP 2005.

Digital Library

[17]

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, and Sergio Maffeis. Language-based defenses against untrusted browser origins. In Presented as part of the 22nd USENIX Security Symposium (USENIX Security 13), pages 653–670, Washington, D.C., 2013. USENIX. ISBN 978-1-931971-03-4.

Digital Library

[18]

Viviana Bono, Michele Bugliesi, and Luigi Liquori. A Lambda Calculus of Incomplete Objects. In Mathematical Foundations of Computer Science 1996, pages 218–229. Springer, 1996.

Digital Library

[19]

[20]

Viviana Bono, Michele Bugliesi, Mariangiola Dezani-Ciancaglini, and Luigi Liquori. Subtyping Constraints for Incomplete Objects. In TAPSOFT’97: Theory and Practice of Software Development, pages 465–477. Springer, 1997.

Digital Library

[21]

[22]

Satish Chandra, Colin S. Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip, and Young-il Choi. Type Inference for Static Compilation of JavaScript. Technical report, Samsung Research America, August 2016.

[23]

Avik Chaudhuri. Personal communication, 2016.

[24]

Philip Wontae Choi, Satish Chandra, George Necula, and Koushik Sen. SJS: A Typed Subset of JavaScript with Fixed Object Layout. Technical Report UCB/EECS-2015- 13, EECS Department, University of California, Berkeley, Apr 2015.

[25]

Wontae Choi, Satish Chandra, George C. Necula, and Koushik Sen. SJS: A Type System for JavaScript with Fixed Object Layout. In Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings, pages 181–198, 2015.

[26]

François Pottier. A Framework for Type Inference with Subtyping. In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP’98), pages 228–238, September 1998.

Digital Library

[27]

François Pottier. Simplifying Subtyping Constraints: A Theory. Information & Computation, 170(2):153–183, November 2001.

Digital Library

[28]

[29]

François Pottier and Didier Rémy. The Essence of ML Type Inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389– 489. MIT Press, 2005.

[30]

Douglas Crockford. JavaScript: The Good Parts. O’Reilly Media, 2008.

Digital Library

[31]

Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLANSIGACT symposium on Principles of programming languages, pages 207–212. ACM, 1982.

Digital Library

[32]

Kathleen Fisher and John C Mitchell. A Delegation-based Object Calculus with Subtyping. In Fundamentals of Computation Theory, pages 42–61. Springer, 1995. 540-60249-6_40.

Digital Library

[33]

Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. The Essence of JavaScript. In European Conference on Object-Oriented Programming (ECOOP), pages 126–150. Springer, 2010.

Digital Library

[34]

Simon Holm Jensen, Anders Møller, and Peter Thiemann. Type Analysis for JavaScript. In SAS, pages 238–255, 2009.

Digital Library

[35]

[36]

Benjamin S. Lerner, Joe Gibbs Politz, Arjun Guha, and Shriram Krishnamurthi. TeJaS: Retrofitting Type Systems for JavaScript. In Proceedings of the 9th Symposium on Dynamic Languages, DLS ’13, pages 1–16, New York, NY, USA, 2013. ACM. ISBN 978-1-4503-2433-5.

Digital Library

[37]

Calvin Loncaric, Satish Chandra, Cole Schlesinger, and Manu Sridharan. A practical framework for type inference error explanation. In Proceedings of the 2016 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA ’16, New York, NY, USA, 2016. ACM.

Digital Library

[38]

Jens Palsberg and Michael I. Schwartzbach. Object-oriented Type Inference. In Conference Proceedings on Object-oriented Programming Systems, Languages, and Applications, OOPSLA ’91, pages 146–161, New York, NY, USA, 1991. ACM.

Digital Library

[39]

ISBN 0-201-55417-8.

[40]

Jens Palsberg and Tian Zhao. Type Inference for Record Concatenation and Subtyping. Inf. Comput., 189(1):54–86, 2004.

Digital Library

[41]

Joe Gibbs Politz, Arjun Guha, and Shriram Krishnamurthi. Semantics and Types for Objects with First-class Member Names. In FOOL 2012: 19th International Workshop on Foundations of Object-Oriented Languages, page 37, 2012.

[42]

Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. The Ins and Outs of Gradual Type Inference. In Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL’12), pages 481–494. ACM, 2012.

Digital Library

[43]

[44]

Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, and Panagiotis Vekris. Safe and Efficient Gradual Typing for TypeScript. In Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL’15). ACM, 2015.

Digital Library

[45]

Didier Rémy. From classes to objects via subtyping. In European Symposium on Programming, pages 200–220. Springer, 1998.

Digital Library

[46]

Didier Rémy and Jérôme Vouillon. Objective ML: An effective object-oriented extension to ML. Theory And Practice of Object Systems, 4(1):27–50, 1998. 9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4.

Digital Library

[47]

Gregor Richards, Sylvain Lebresne, Brian Burg, and Jan Vitek. An Analysis of the Dynamic Behavior of JavaScript Programs. PLDI ’10, pages 1–12, New York, NY, USA, 2010. ACM. ISBN 978-1-4503-0019-3.

Digital Library

[48]

Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete Types for TypeScript. In John Tang Boyland, editor, 29th European Conference on Object-Oriented Programming (ECOOP 2015), volume 37 of Leibniz International Proceedings in Informatics (LIPIcs), pages 76– 100, Dagstuhl, Germany, 2015. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. ISBN 978-3-939897-86-6.

[49]

Jeremy G Siek, Michael M Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. Monotonic References for Efficient Gradual Typing. In European Symposium on Programming Languages and Systems, ESOP, pages 432–456. Springer, 2015.

Digital Library

[50]

Peter Thiemann. Towards a Type System for Analyzing Javascript Programs. In ESOP 2005. ISBN 3-540-25435-8, 978-3-540-25435-5.

Digital Library

[51]

Valery Trifonov and Scott F. Smith. Subtyping Constrained Types. In Static Analysis, Third International Symposium, SAS’96, Aachen, Germany, September 24-26, 1996, Proceedings, pages 349–365, 1996.

Digital Library

[52]

Michael M Vitousek, Andrew M Kent, Jeremy G Siek, and Jim Baker. Design and Evaluation of Gradual Typing for Python. In Dynamic Language Symposium (DLS). ACM, 2014.

Digital Library

[53]

[54]

Mitchell Wand. Complete Type Inference for Simple Objects. In LICS, volume 87, pages 37–44, 1987.

[55]

Mitchell Wand. Type Inference for Record Concatenation and Multiple Inheritance. In Logic in Computer Science, 1989. LICS’89, Proceedings., Fourth Annual Symposium on, pages 92–97. IEEE, 1989. Introduction Overview Type System Requirements The Type System Inference Challenges Terms, Types, and Constraint Generation Terms Types Subtyping and Type Equivalence Constraint Language Constraint Generation Constraint Solving Type Propagation Type Ascription Soundness of Type Inference Evaluation Practical Considerations Explanation of Workarounds More Problematic Constructs The Promise of Ahead-of-Time Compilation Related Work

Digital Library

Cited By

Guo YChen ZChen LXu WLi YZhou YXu B(2024)Generating Python Type Annotations from Type Inference: How Far Are We?ACM Transactions on Software Engineering and Methodology10.1145/365215333:5(1-38)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3652153
Stallenberg DOlsthoorn MPanichella A(2022)Guess What: Test Case Generation for Javascript with Unsupervised Probabilistic Type InferenceSearch-Based Software Engineering10.1007/978-3-031-21251-2_5(67-82)Online publication date: 17-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-21251-2_5
Serrano M(2021)Of JavaScript AOT compilation performanceProceedings of the ACM on Programming Languages10.1145/34735755:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473575
Show More Cited By

Index Terms

Type inference for static compilation of JavaScript
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. General programming languages
      1. Language features

Recommendations

Type inference for static compilation of JavaScript
OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive ...
Type elaboration and subtype completion for Java bytecode

Java source code is strongly typed, but the translation from Java source to bytecode omits much of the type information originally contained within methods. Type elaboration is a technique for reconstructing strongly typed programs from incompletely ...
Polymorphic type inference and abstract data types

Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned 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 51, Issue 10

OOPSLA '16

October 2016

915 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3022671

Editor:
Matthew Fluet

Issue’s Table of Contents

OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
October 2016
915 pages
ISBN:9781450344449
DOI:10.1145/2983990
General Chair:
Eelco Visser
Delft University of Technology, Netherlands
,
Program Chair:
Yannis Smaragdakis
University of Athens, Greece

Copyright © 2016 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 ACM 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: 19 October 2016

Published in SIGPLAN Volume 51, Issue 10

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
550
Total Downloads

Downloads (Last 12 months)53
Downloads (Last 6 weeks)8

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Guo YChen ZChen LXu WLi YZhou YXu B(2024)Generating Python Type Annotations from Type Inference: How Far Are We?ACM Transactions on Software Engineering and Methodology10.1145/365215333:5(1-38)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3652153
Stallenberg DOlsthoorn MPanichella A(2022)Guess What: Test Case Generation for Javascript with Unsupervised Probabilistic Type InferenceSearch-Based Software Engineering10.1007/978-3-031-21251-2_5(67-82)Online publication date: 17-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-21251-2_5
Serrano M(2021)Of JavaScript AOT compilation performanceProceedings of the ACM on Programming Languages10.1145/34735755:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473575
Wang PBangert JKern C(2021)If It's Not Secure, It Should Not CompileProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00123(1360-1372)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00123
Zhuo XZhang C(2020)TFA: an efficient and precise virtual method call resolution for JavaFormal Aspects of Computing10.1007/s00165-020-00518-z32:4-6(395-416)Online publication date: 6-Oct-2020
https://dl.acm.org/doi/10.1007/s00165-020-00518-z
Ugawa TIwasaki HKataoka T(2019)Collecting Type Information Using Unit Tests for Customizing JavaScript Virtual MachinesProceedings of the 14th Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems10.1145/3340670.3342425(1-4)Online publication date: 19-Jul-2019
https://dl.acm.org/doi/10.1145/3340670.3342425
Grech NFischer BRathke J(2018)Preemptive type checkingJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2018.08.003101(151-181)Online publication date: Dec-2018
https://doi.org/10.1016/j.jlamp.2018.08.003
Wu JLemieux C(2024)QuAC: Quick Attribute-Centric Type Inference for PythonProceedings of the ACM on Programming Languages10.1145/36897838:OOPSLA2(2040-2069)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689783
Belyakova JChung BTate RVitek J(2024)Decidable Subtyping of Existential Types for JuliaProceedings of the ACM on Programming Languages10.1145/36564218:PLDI(1091-1114)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656421
Toufie ZKabaso B(2024)Os noise mitigations for benchmarking web browser execution environment performanceDiscover Computing10.1007/s10791-024-09471-427:1Online publication date: 29-Oct-2024
https://doi.org/10.1007/s10791-024-09471-4
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents