Mixed Messages: Measuring Conformance and Non-Interference in TypeScript

Authors Jack Williams, J. Garrett Morris, Philip Wadler, Jakub Zalewski



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.28.pdf
  • Filesize: 0.5 MB
  • 29 pages

Document Identifiers

Author Details

Jack Williams
J. Garrett Morris
Philip Wadler
Jakub Zalewski

Cite AsGet BibTex

Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 28:1-28:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.28

Abstract

TypeScript participates in the recent trend among programming languages to support gradual typing. The DefinitelyTyped Repository for TypeScript supplies type definitions for over 2000 popular JavaScript libraries. However, there is no guarantee that implementations conform to their corresponding declarations. We present a practical evaluation of gradual typing for TypeScript. We have developed a tool for use with TypeScript, based on the polymorphic blame calculus, for monitoring JavaScript libraries and TypeScript clients against the TypeScript definition. We apply our tool, TypeScript TPD, to those libraries in the DefinitelyTyped Repository which had adequate test code to use. Of the 122 libraries we checked, 62 had cases where either the library or its tests failed to conform to the declaration. Gradual typing should satisfy non-interference. Monitoring a program should never change its behaviour, except to raise a type error should a value not conform to its declared type. However, our experience also suggests serious technical concerns with the use of the JavaScript proxy mechanism for enforcing contracts. Of the 122 libraries we checked, 22 had cases where the library or its tests violated non-interference.
Keywords
  • Gradual Typing
  • TypeScript
  • JavaScript
  • Proxies

Metrics

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

References

  1. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for All. In ACM Symposium on Principles of Programming Languages (POPL), 2011. URL: http://dx.doi.org/10.1145/1925844.1926409.
  2. Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. Theorems for Free for Free: Parametricity, With and Without Types. In ACM International Conference on Functional Programming (ICFP), 2017. Google Scholar
  3. Thomas H. Austin, Tim Disney, and Cormac Flanagan. Virtual Values for Language Extension. In ACM Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA), 2011. URL: http://dx.doi.org/10.1145/2076021.2048136.
  4. Gavin Bierman, Martín Abadi, and Mads Torgersen. Understanding typescript. In European Conference on Object-Oriented Programming (ECOOP), 2014. URL: http://dx.doi.org/10.1007/978-3-662-44202-9_11.
  5. DefinitelyTyped. DefinitelyTyped repository. https://github.com/DefinitelyTyped/DefinitelyTyped, May 2017.
  6. Oli Evans and Alan Shaw. asciify. https://github.com/olizilla/asciify, May 2017.
  7. Asger Feldthaus and Anders Møller. Checking correctness of typescript interfaces for javascript libraries. In ACM Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA), 2014. URL: http://dx.doi.org/10.1145/2714064.2660215.
  8. Robert Bruce Findler and Matthias Felleisen. Contracts for Higher-order Functions. In ACM International Conference on Functional Programming (ICFP), 2002. URL: http://dx.doi.org/10.1145/583852.581484.
  9. Jeff Goddard. swiz.d.ts. https://github.com/borisyankov/DefinitelyTyped/tree/master/types/swiz/index.d.ts, May 2017.
  10. Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. Relationally-parametric Polymorphic Contracts. In Dynamic Languages Symposium (DLS), 2007. URL: http://dx.doi.org/10.1145/1297081.1297089.
  11. Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann. Transparent Object Proxies in JavaScript. In European Conference on Object-Oriented Programming (ECOOP), 2015. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2015.149.
  12. Matthias Keil and Peter Thiemann. On the proxy identity crisis. CoRR, 2013. Google Scholar
  13. Matthias Keil and Peter Thiemann. Blame assignment for higher-order contracts with intersection and union. In ACM International Conference on Functional Programming (ICFP), 2015. URL: http://dx.doi.org/10.1145/2858949.2784737.
  14. Erik Krogh Kristensen and Anders Møller. Inference and evolution of typescript declaration files. In Proc. 20th International Conference on Fundamental Approaches to Software Engineering (FASE), 2017. URL: http://dx.doi.org/10.1007/978-3-662-54494-5_6.
  15. Gianluca Mezzetti, Anders Møller, and Fabio Strocco. Type Unsoundness in Practice: An Empirical Study of Dart. In Dynamic Languages Symposium (DLS), 2016. URL: http://dx.doi.org/10.1145/2989225.2989227.
  16. Microsoft. TypeScript language specification. https://github.com/Microsoft/TypeScript/blob/master/doc/spec.md, January 2016.
  17. Alan Norbauer. asciify.d.ts. https://github.com/DefinitelyTyped/DefinitelyTyped/blob/master/types/asciify/index.d.ts, May 2016.
  18. Rackspace. node-swiz. https://github.com/racker/node-swiz, May 2017.
  19. Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, and Panagiotis Vekris. Safe &Efficient Gradual Typing for TypeScript. In ACM Symposium on Principles of Programming Languages (POPL), 2015. URL: http://dx.doi.org/10.1145/2775051.2676971.
  20. John Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing, 1983. Google Scholar
  21. Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete Types for TypeScript. In European Conference on Object-Oriented Programming (ECOOP), 2015. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2015.76.
  22. Rob Richardson. gulp-if. https://github.com/robrich/gulp-if, May 2017.
  23. Jeremy Siek and Walid Taha. Gradual typing for objects. In European Conference on Object-Oriented Programming (ECOOP), 2007. URL: http://dx.doi.org/10.1007/978-3-540-73589-2_2.
  24. Jeremy G. Siek and Walid Taha. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme), 2006. Google Scholar
  25. 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 (ESOP), 2015. URL: http://dx.doi.org/10.1007/978-3-662-46669-8_18.
  26. Kieran Simpson. clone.d.ts. https://github.com/DefinitelyTyped/DefinitelyTyped/blob/master/types/clone/index.d.ts, May 2017.
  27. Joe Skeen and Asana. gulp-if.d.ts. https://github.com/DefinitelyTyped/DefinitelyTyped/blob/master/types/gulp-if/index.d.ts, May 2017.
  28. T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. Chaperones and Impersonators: Run-time Support for Reasonable Interposition. In ACM Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA), 2012. URL: http://dx.doi.org/10.1145/2384616.2384685.
  29. Nikhil Swamy, Cedric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin Bierman. Gradual Typing Embedded Securely in JavaScript. In ACM Symposium on Principles of Programming Languages (POPL), 2014. URL: http://dx.doi.org/10.1145/2578855.2535889.
  30. Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. Is Sound Gradual Typing Dead? In ACM Symposium on Principles of Programming Languages (POPL), 2016. URL: http://dx.doi.org/10.1145/2837614.2837630.
  31. Peter Thiemann. Towards a Type System for Analyzing JavaScript Programs. In European Symposium on Programming (ESOP), 2005. URL: http://dx.doi.org/10.1007/978-3-540-31987-0_28.
  32. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage Migration: From Scripts to Programs. In Dynamic Languages Symposium (DLS), 2006. URL: http://dx.doi.org/10.1145/1176617.1176755.
  33. Tom Van Cutsem and Mark S. Miller. Proxies: Design Principles for Robust Object-oriented Intercession APIs. In Dynamic Languages Symposium (DLS), 2010. URL: http://dx.doi.org/10.1145/1899661.1869638.
  34. Tom Van Cutsem and Mark S. Miller. Trustworthy proxies: Virtualizing objects with invariants. In European Conference on Object-Oriented Programming (ECOOP), 2013. URL: http://dx.doi.org/10.1007/978-3-642-39038-8_7.
  35. Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. Design and Evaluation of Gradual Typing for Python. In Dynamic Languages Symposium (DLS), 2014. URL: http://dx.doi.org/10.1145/2775052.2661101.
  36. Paul Vorbach. node-clone. https://github.com/pvorb/node-clone, May 2017.
  37. Philip Wadler. Theorems for free! In ACM Conference on Functional Programming Languages and Computer Architecture (FPCA), 1989. URL: http://dx.doi.org/10.1145/99370.99404.
  38. Philip Wadler. A complement to blame. In Summit on Advances in Programming Languages (SNAPL), 2015. URL: http://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.309.
  39. Philip Wadler and Robert Bruce Findler. Well-typed programs can’t be blamed. In European Symposium on Programming (ESOP), 2009. URL: http://dx.doi.org/10.1007/978-3-642-00590-9_1.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail