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.

Full paper

o

Presented at FOOL'09; Saturday, 24 January 2009, Savannah, Georgia, USA.