zbMATH — the first resource for mathematics

Preemptive type checking. (English) Zbl 1400.68056
Summary: Dynamically typed languages are very well suited for rapid prototyping, agile programming methodologies and rapidly evolving software. However, programmers can still benefit from the ability to detect type errors in their code early, in particular if this does not impose restrictions on their programming style.
In this paper we describe a new type checking system that identifies potential type errors in such languages through a flow-sensitive static analysis. It computes for every expression the variable’s present (from the values that it has last been assigned) and future (with which it is used in the further program execution) types, respectively. Using this information, the mechanism inserts type checks at strategic points in the original program. We prove that these checks are inserted as early as possible and preempt type errors earlier than existing type systems. We further show that these checks do not change the semantics of programs that do not raise type errors.
Preemptive type checking can be added to existing languages without the need to modify the existing runtime environment. Instead, it can be invoked at a very late stage, after the compilation to bytecode and initialisation of the program. We demonstrate an implementation of this for the Python language, and its effectiveness on a number of standard benchmarks.
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N15 Theory of programming languages
68N18 Functional programming and lambda calculus
Flow; Hack; Python
Full Text: DOI
[1] TIOBE programming community index, (July 2015), Tech. Rep.
[2] Ray, B.; Posnett, D.; Filkov, V.; Devanbu, P. T., A large scale study of programming languages and code quality in github, (Proceedings of FSE, (2014))
[3] Hoenicke, J.; Leino, K. R.M.; Podelski, A.; Schäf, M.; Wies, T., Doomed program points, Form. Methods Syst. Des., 37, 2, 171-199, (2010) · Zbl 1211.68090
[4] Cartwright, R.; Fagan, M., Soft typing, (Proceedings of PLDI, (1991)), 278-292
[5] Vitousek, M. M.; Kent, A. M.; Siek, J. G.; Baker, J., Design and evaluation of gradual typing for python, (Proceedings of DLS, (2015))
[6] Grech, N.; Rathke, J.; Fischer, B., Preemptive type checking in dynamically typed languages, (Proceedings of the 10th International Colloquium on Theoretical Aspects of Computing, Lecture Notes in Computer Science, vol. 8049, (2013), Springer), 195-212 · Zbl 1405.68030
[7] Andersen, L. O., Program analysis and specialization for the C programming language, (May 1994), DIKU, University of Copenhagen, Ph.D. thesis
[8] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Proceedings of POPL, (1977)) · Zbl 0788.68094
[9] Siek, J.; Vachharajani, M., Gradual typing with unification-based inference, (Proceedings of DLS, (2008))
[10] Abadi, M.; Cardelli, L.; Pierce, B.; Plotkin, G., Dynamic typing in a statically typed language, ACM Trans. Program. Lang. Syst., 13, 2, 237-268, (1991)
[11] Wrigstad, T.; Nardelli, F. Z.; Lebresne, S.; Östlund, J.; Vitek, J., Integrating typed and untyped code in a scripting language, (Proceedings of POPL, (2010)), 377-388 · Zbl 1312.68048
[12] Ancona, D.; Ancona, M.; Cuni, A.; Matsakis, N. D., Rpython: a step towards reconciling dynamically and statically typed OO languages, (Proceedings of DLS, (2007)), 53-64
[13] Borning, A. H.; Ingalls, D. H.H., A type declaration and inference system for smalltalk, (Proceedings of POPL, (1982)), 133-141
[14] Agesen, O.; Palsberg, J.; Schwartzbach, M. I., Type inference of SELF: analysis of objects with dynamic and multiple inheritance, (Proceedings of ECOOP, (1993)), 247-267
[15] Livshits, B.; Sridharan, M.; Smaragdakis, Y.; Lhoták, O.; Amaral, J. N.; Chang, B.-Y. E.; Guyer, S. Z.; Khedker, U. P.; Møller, A.; Vardoulakis, D., In defense of soundiness: a manifesto, Commun. ACM, 58, 2, 44-46, (2015)
[16] Winter, C.; Lownds, T., Python enhancement proposal (PEP) 3107, Available online:
[17] Grech, N.; Fourtounis, G.; Francalanza, A.; Smaragdakis, Y., Heaps don’t Lie: countering unsoundness with heap snapshots, OOPSLA, Proc. ACM Programm. Lang., 1, (2018)
[18] Grech, N.; Fourtounis, G.; Francalanza, A.; Smaragdakis, Y., Shooting from the heap: ultra-scalable static analysis with heap snapshots, (International Symposium on Software Testing and Analysis (ISSTA), ISSTA ’18, (2018), ACM New York, NY, USA)
[19] Shivers, O., Control-flow analysis of higher-order languages, (1991), Carnegie Mellon University, Ph.D. thesis
[20] The computer language benchmarks game, (2013)
[21] Siek, J.; Taha, W., Gradual typing for functional languages, (Proceedings of Scheme and Functional Programming Workshop, (2006))
[22] Takikawa, A.; Feltey, D.; Greenman, B.; New, M. S.; Vitek, J.; Felleisen, M., Is sound gradual typing dead?, (Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’16, (2016), ACM New York, NY, USA), 456-468
[23] Richards, G.; Arteca, E.; Turcotte, A., The VM already knew that: leveraging compile-time knowledge to optimize gradual typing, Proc. ACM Program. Lang., 1, OOPSLA, 55:1-55:27, (2017)
[24] Bierman, G. M.; Abadi, M.; Torgersen, M., Understanding typescript, (Proceedings of ECOOP, (2014))
[25] Rastogi, A.; Swamy, N.; Fournet, C.; Bierman, G.; Vekris, P., Safe & efficient gradual typing for typescript, (Proceedings of POPL, (2015)) · Zbl 1346.68049
[26] A. Chaudhuri, B. Hosmer, G. Levi, Flow, a new static type checker for JavaScript, 2014.
[27] J. Verlaguet, A. Menghrajani, Hack: a new programming language for HHVM, 2014.
[28] Wright, A. K.; Cartwright, R., A practical soft type system for scheme, ACM Trans. Program. Lang. Syst., 19, 87-152, (1997)
[29] Salib, M., Starkiller: A static type inferencer and compiler for python, (2004), Department of Electrical Engineering and Computer Science, MIT, Masters Thesis
[30] Nyström, S.-O., A soft-typing system for Erlang, (Proceedings of Erlang Workshop, (2003)), 56-71
[31] Bracha, G., Pluggable type systems, (OOPSLA Workshop on Revival of Dynamic Languages, (2004))
[32] Choi, W.; Chandra, S.; Necula, G. C.; Sen, K., Sjs: a type system for javascript with fixed object layout, (Blazy, S.; Jensen, T., SAS, Lecture Notes in Computer Science, vol. 9291, (2015), Springer), 181-198
[33] Chandra, S.; Gordon, C. S.; Jeannin, J.-B.; Schlesinger, C.; Sridharan, M.; Tip, F.; Choi, Y., Type inference for static compilation of javascript, SIGPLAN Not., 51, 10, 410-429, (2016)
[34] Hackett, B.; Guo, S.-y., Fast and precise hybrid type inference for javascript, (Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, (2012), ACM New York, NY, USA), 239-250
[35] Jensen, S. H.; Møller, A.; Thiemann, P., Type analysis for javascript, (Proceedings of the 16th International Symposium on Static Analysis, SAS ’09, (2009), Springer-Verlag Berlin, Heidelberg), 238-255
[36] Lerner, B. S.; Politz, J. G.; Guha, A.; Krishnamurthi, S., Tejas: retrofitting type systems for javascript, SIGPLAN Not., 49, 2, 1-16, (2013)
[37] Tobin-Hochstadt, S.; Felleisen, M., The design and implementation of typed scheme, (Proceedings of POPL, (2008)), 395-406 · Zbl 1295.68055
[38] Furr, M.; An, J.-h. D.; Foster, J. S.; Hicks, M., Static type inference for ruby, (Symposium on Applied Computing, (2009)), 1859-1866
[39] Heidegger, P.; Thiemann, P., Recency types for dynamically-typed, object-based languages, (Proceedings of FOOL, (2009))
[40] Winskel, G., A note on model checking the modal μ-calculus, Theor. Comput. Sci., 83, 1, 157-167, (1991) · Zbl 0745.68083
[41] Simon, L.; Bansal, A.; Mallya, A.; Gupta, G., Co-logic programming: extending logic programming with coinduction, (Proceedings of International Colloquium on Automata, Languages and Programming, ICALP, LNCS, vol. 4596, (2007), Springer-Verlag) · Zbl 1171.68404
[42] Ancona, D., Regular corecursion in prolog, Comput. Lang. Syst. Struct., 39, 4, 142-162, (2013), special issue on the Programming Languages track at the 27th ACM Symposium on Applied Computing
[43] Ancona, D.; Lagorio, G.; Zucca, E., Type inference by coinductive logic programming, (Types for Proofs and Programs, LNCS, vol. 5497, (2008)), 1-18 · Zbl 1246.68079
[44] Ancona, D.; Lagorio, G., Coinductive type systems for object-oriented languages, (Proceedings of the 23rd European Conference on ECOOP 2009 - Object-Oriented Programming, Genoa, (2009), Springer-Verlag Berlin, Heidelberg), 2-26
[45] DeVries, B. W.; Gupta, G.; Hamlen, K. W.; Moore, S.; Sridhar, M., Actionscript bytecode verification with co-logic programming, (Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS ’09, (2009), ACM New York, NY, USA), 9-15
[46] Shivers, O., Control-flow analysis in scheme, (Proceedings of PLDI, (1988)), 164-174
[47] Lerch, J.; Späth, J.; Bodden, E.; Mezini, M., Access-path abstraction: scaling field-sensitive data-flow analysis with unbounded access paths (T), (30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015, (2015)), 619-629
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.