Type safety analysis for Dart
Abstract
Optional typing is traditionally viewed as a compromise between static and dynamic type checking, where code without type annotations is not checked until runtime. We demonstrate that optional type annotations in Dart programs can be integrated into a flow analysis to provide static type safety guarantees both for annotated and non-annotated parts of the code. We explore two approaches: one that uses type annotations for filtering, and one that uses them as specifications. What makes this particularly challenging for Dart is that its type system is unsound even for fully annotated code. Experimental results show that the technique is remarkably effective, even without context sensitivity: 99.3% of all property lookup operations are reported type safe in a collection of benchmark programs.
References
[1]
O. Agesen. The cartesian product algorithm: Simple and precise type inference of parametric polymorphism. In Object-Oriented Programming, 9th European Conference (ECOOP), 1995.
[2]
G. Bracha and D. Ungar. Mirrors: design principles for meta-level facilities of object-oriented programming languages. In Proc. ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2004.
[3]
E. Brandt. Why Dart types are optional and unsound, 2011. https: //www.dartlang.org/articles/why-dart-types/.
[4]
R. Cartwright and M. Fagan. Soft typing. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 1991.
[5]
D. R. Chase, M. Wegman, and F. K. Zadeck. Analysis of pointers and structures. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 1990.
[6]
J. Dean, D. Grove, and C. Chambers. Optimization of object-oriented programs using static class hierarchy analysis. In Proc. Object-Oriented Programming, 9th European Conference (ECOOP), 1995.
[7]
Ecma International. Dart Programming Language Specification, ECMA-408, 4th Edition, December 2015.
[8]
E. Ernst, A. Møller, M. Schwarz, and F. Strocco. Message safety in Dart. Science of Computer Programming, 2016. In press. Earlier version in Proc. 11th Dynamic Languages Symposium (DLS), 2015.
[9]
Facebook Inc. Flow – a static type checker for JavaScript, 2016. http://flowtype.org/.
[10]
C. Flanagan, M. Flatt, S. Krishnamurthi, S. Weirich, and M. Felleisen. Catching bugs in the web of program invariants. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 1996.
[11]
Google Inc. Strong mode, 2015. https://github.com/dart-lang/ dev_compiler/blob/master/STRONG_MODE.md.
[12]
Google Inc. dart2js, 2016. https://www.dartlang.org/tools/ dart2js/.
[13]
Google Inc. dartanalyzer, 2016. https://github.com/dart-lang/ analyzer_cli.
[14]
R. Hasti and S. Horwitz. Using static single assignment form to improve flow-insensitive pointer analysis. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 1998.
[15]
N. Heintze. Set-based analysis of ML programs. In LISP and Functional Programming, pages 306–317, 1994.
[16]
S. H. Jensen, A. Møller, and P. Thiemann. Type analysis for JavaScript. In Proc. 16th International Static Analysis Symposium (SAS), 2009.
[17]
H. Mehnert. Extending Dylan’s type system for better type inference and error detection. In International Lisp Conference (ILC), 2010.
[18]
F. Ortin. Type inference to optimize a hybrid statically and dynamically typed language. Comput. J., 54(11):1901–1924, 2011.
[19]
J. Palsberg and M. I. Schwartzbach. Safety analysis versus type inference. Inf. Comput., 118(1), 1995.
[20]
A. Rastogi, A. Chaudhuri, and B. Hosmer. The ins and outs of gradual type inference. In Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2012.
[21]
J. G. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006.
[22]
J. G. Siek and M. Vachharajani. Gradual typing with unification-based inference. In Proc. Symposium on Dynamic Languages (DLS), 2008.
[23]
J. G. Siek, P. Thiemann, and P. Wadler. Blame and coercion: together again for the first time. In Proc. 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2015.
[24]
J. G. Siek, M. M. Vitousek, M. Cimini, and J. T. Boyland. Refined criteria for gradual typing. In Proc. 1st Summit on Advances in Programming Languages (SNAPL), 2015.
[25]
M. Sridharan, S. Chandra, J. Dolby, S. J. Fink, and E. Yahav. Alias analysis for object-oriented programs. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, volume 7850 of LNCS, pages 196–232. Springer, 2013.
[26]
A. Takikawa, D. Feltey, B. Greenman, M. S. New, J. Vitek, and M. Felleisen. Is sound gradual typing dead? In Proc. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016.
[27]
The Mypy Project. mypy – optional static typing for Python, 2016. https://mypy-lang.org/.
Index Terms
- Type safety analysis for Dart
Recommendations
Message safety in Dart
DLS 2015: Proceedings of the 11th Symposium on Dynamic LanguagesUnlike traditional static type checking, the type system in the Dart programming language is unsound by design, even for fully annotated programs. The rationale has been that this allows compile-time detection of likely errors and enables code ...
Type safety analysis for Dart
DLS 2016: Proceedings of the 12th Symposium on Dynamic LanguagesOptional typing is traditionally viewed as a compromise between static and dynamic type checking, where code without type annotations is not checked until runtime. We demonstrate that optional type annotations in Dart programs can be integrated into a ...
Message safety in Dart
DLS '15Unlike traditional static type checking, the type system in the Dart programming language is unsound by design, even for fully annotated programs. The rationale has been that this allows compile-time detection of likely errors and enables code ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
February 2017
131 pages
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: 01 November 2016
Published in SIGPLAN Volume 52, Issue 2
Check for updates
Author Tags
Qualifiers
- Article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations6Total Citations
- 182Total Downloads
- Downloads (Last 12 months)11
- Downloads (Last 6 weeks)0
Reflects downloads up to 23 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in