Trace Typing: An Approach for Evaluating Retrofitted Type Systems

Authors Esben Andreasen, Colin S. Gordon, Satish Chandra, Manu Sridharan, Frank Tip, Koushik Sen

Thumbnail PDF


  • Filesize: 0.76 MB
  • 26 pages

Document Identifiers

Author Details

Esben Andreasen
Colin S. Gordon
Satish Chandra
Manu Sridharan
Frank Tip
Koushik Sen

Cite AsGet BibTex

Esben Andreasen, Colin S. Gordon, Satish Chandra, Manu Sridharan, Frank Tip, and Koushik Sen. Trace Typing: An Approach for Evaluating Retrofitted Type Systems. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 1:1-1:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Recent years have seen growing interest in the retrofitting of type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity, or performance. In such cases, type system developers must strike a delicate balance between disallowing certain coding patterns to keep the type system simple, or including them at the expense of additional complexity and effort. Thus far, the process for designing retrofitted type systems has been largely ad hoc, because evaluating multiple variations of a type system on large bodies of existing code is a significant undertaking. We present trace typing: a framework for automatically and quantitatively evaluating variations of a retrofitted type system on large code bases. The trace typing approach involves gathering traces of program executions, inferring types for instances of variables and expressions occurring in a trace, and merging types according to merge strategies that reflect specific (combinations of) choices in the source-level type system design space. We evaluated trace typing through several experiments. We compared several variations of type systems retrofitted onto JavaScript, measuring the number of program locations with type errors in each case on a suite of over fifty thousand lines of JavaScript code. We also used trace typing to validate and guide the design of a new retrofitted type system that enforces fixed object layout for JavaScript objects. Finally, we leveraged the types computed by trace typing to automatically identify tag tests --- dynamic checks that refine a type --- and examined the variety of tests identified.
  • Retrofitted type systems
  • Type system design
  • trace typing


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Beatrice Åkerblom and Tobias Wrigstad. Measuring polymorphism in Python programs. In Proceedings of the 11th Symposium on Dynamic Languages (DLS), 2015. Google Scholar
  2. Jong-hoon David An, Avik Chaudhuri, Jeffrey S Foster, and Michael Hicks. Dynamic Inference of Static Types for Ruby. In POPL, 2011. Google Scholar
  3. Chris Andreae, James Noble, Shane Markstrum, and Todd Millstein. A Framework for Implementing Pluggable Type Systems. In OOPSLA, 2006. Google Scholar
  4. Esben Andreasen, Colin S. Gordon, Satish Chandra, Manu Sridharan, Frank Tip, and Koushik Sen. Trace Typing: An Approach for Evaluating Retrofitted Type Systems (Extended Version). Technical Report SRA-CSIC-2016-001, Samsung Research America, 2016. URL:
  5. Gavin Bierman, Martín Abadi, and Mads Torgersen. Understanding TypeScript. In ECOOP, 2014. Google Scholar
  6. Gilad Bracha. Pluggable Type Systems. In OOPSLA Workshop on Revival of Dynamic Languages, 2004. Google Scholar
  7. Robert Cartwright and Mike Fagan. Soft Typing. In PLDI, 1991. Google Scholar
  8. Avik Chaudhuri. Bounded Polymorphism. URL:
  9. Philip Wontae Choi, Satish Chandra, George Necula, and Koushik Sen. SJS: A Type System for JavaScript with Fixed Object Layout. In SAS, 2015. Google Scholar
  10. Ravi Chugh, David Herman, and Ranjit Jhala. Dependent Types for JavaScript. In OOPSLA, 2012. Google Scholar
  11. Devin Coughlin, Bor-Yuh Evan Chang, Amer Diwan, and Jeremy G. Siek. Measuring enforcement windows with symbolic trace interpretation: What well-behaved programs say. In ISSTA, 2012. Google Scholar
  12. Werner Dietl, Stephanie Dietzel, Michael D Ernst, Kivanç Muşlu, and Todd W Schiller. Building and Using Pluggable Type-Checkers. In ICSE, 2011. Google Scholar
  13. Facebook. Flow: A Static Type Checker for JavaScript.
  14. Ronald Garcia, Alison M. Clark, and Éric Tanter. Abstracting Gradual Typing. In POPL, 2016. Google Scholar
  15. Jacques Garrigue. Relaxing the Value Restriction. In Functional and Logic Programming, 2004. Google Scholar
  16. Google. Closure.
  17. Colin S Gordon, Werner Dietl, Michael D Ernst, and Dan Grossman. JavaUI: Effects for Controlling UI Object Access. In ECOOP, 2013. Google Scholar
  18. Ben Greenman, Fabian Muehlboeck, and Ross Tate. Getting F-bounded Polymorphism into Shape. In PLDI, 2014. Google Scholar
  19. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. The Essence of JavaScript. In ECOOP, 2010. Google Scholar
  20. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. Typing Local Control and State Using Flow Analysis. In ESOP, 2011. Google Scholar
  21. Benjamin S Lerner, Joe Gibbs Politz, Arjun Guha, and Shriram Krishnamurthi. TeJaS: Retrofitting Type Systems for JavaScript. In DLS, 2013. Google Scholar
  22. Microsoft. TypeScript Handbook.
  23. Matthew M Papi, Mahmood Ali, Telmo Luis Correa Jr, Jeff H Perkins, and Michael D Ernst. Practical Pluggable Types for Java. In ISSTA, 2008. Google Scholar
  24. Joe Gibbs Politz, Arjun Guha, and Shriram Krishnamurthi. Semantics and Types for Objects with First-Class Member Names. In FOOL, 2012. Google Scholar
  25. Claudiu Saftoiu, Arjun Guha, and Shriram Krishnamurthi. Runtime Type-Discovery for JavaScript. Technical Report CS-10-05, Brown University, 2010. Google Scholar
  26. Koushik Sen, Swaroop Kalasapur, Tasneem Brutch, and Simon Gibbs. Jalangi: A selective record-replay and dynamic analysis framework for JavaScript. In FSE, 2013. Google Scholar
  27. Frederick Smith, David Walker, and Greg Morrisett. Alias Types. In ESOP, 2000. Google Scholar
  28. Sam Tobin-Hochstadt and Matthias Felleisen. Logical Types for Untyped Languages. In ICFP, 2010. Google Scholar
  29. Jonathan Turner. Announcing TypeScript 1.4. URL:
  30. Andrew K. Wright. Simple Imperative Polymorphism. LISP and Symbolic Computation, 8(4):343-355, 1995. Google Scholar
  31. Andrew K. Wright and Robert Cartwright. A Practical Soft Type System for Scheme. ACM TOPLAS, 19(1):87-152, January 1997. URL:
  32. Haiping Zhao, Iain Proctor, Minghui Yang, Xin Qi, Mark Williams, Qi Gao, Guilherme Ottoni, Andrew Paroski, Scott MacVicar, Jason Evans, and Stephen Tu. The HipHop Compiler for PHP. In OOPSLA, 2012. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail