Recency Types for Dynamically-Typed, Object-Based
Languages
Phillip Heidegger and Peter Thiemann
Abstract
Object-based languages with dynamic type systems are popular because
they accelerate the development of short programs. As larger programs
are built with those languages, static analyses become important tools
for detecting programming errors.
We define such an analysis as a type system for an imperative
object-based calculus and prove its type soundness. The calculus models
essential features of the JavaScript language, as an example of a
typical and widely used dynamically-typed, object-based language. The
model includes objects as property maps, type change during object
initialization, and precise support for JavaScript's prototype
mechanism.
As a more general technical contribution, our work demonstrates that
the idea of recency abstraction can be transferred from abstract
interpretation to a type system. We model recency information with a
notion of precise object pointers that enables strong, type changing
updates of object types during a generalized initialization phase. The
same precise object pointers allow for an accurate treatment of the
prototype mechanism. Unlike linear types, precise object pointers can
be nested and mixed arbitrarily with ordinary, imprecise object
pointers in the type of a data structure.
Presented at FOOL'09; Saturday, 24 January
2009, Savannah, Georgia, USA.