Preemptive type checking in dynamically typed programs
Neville Grech
School of Electronics and Computer Science
University of Southampton
Wednesday, 8 December 2010, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: In dynamically typed languages, the type of a variable is assigned as a result of a computation that occurs at runtime. Since the types of variables can change at runtime, this entails that a type-safety guarantee is generally not statically computable. Instead, type checking is performed on the fly at runtime. Early type error detection is practically non-existent in such languages. Existing type systems that try to mitigate this problem try to enforce a statically typed semantics to a dynamic language and consequently end up severely reducing the expressiveness of such a language.
We present a method where most invalid runs of a program can be identified in advance through a flow-sensitive static type checking mechanism. To allow dynamicity, the program is transformed and type safety assertions are inserted at the earliest point where a type error may be determined, thus preempting any type errors from happening. This process is handled by propagating constraints derived from the program itself through the control flow graph. These assertions do not reduce the expressiveness of the language in which the program is implemented but merely raise errors before they can actually happen in practice. Errors that are detected early can be fixed immediately, rather than lurking in the code to be discovered much later, perhaps after the program has been deployed. Also, if an error is detected in the middle of some transactional code, the program can bail out before the transaction is initiated.
After inserting type assertions, we aim to guarantee that the resulting program is well-typed if the assertions can be guaranteed to hold. We would also like to show that a program that can be statically shown to be ill-typed will fail through a type-safety assertion inserted at the beginning of the program. Also, by extension, the program will never raise a type error if no type safety assertions for that program needs to be inserted.
Tarmo Uustalu
Last update 9.12.2010