Gradual Typing for Generics

Lintaro Ina and Atsushi Igarashi. To appear in Proceeding of the ACM International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2011), Portland, OR, October, 2011. An earlier version titled "Towards Gradual Typing for Generics" appeared in Proceedings of the 1st International Workshop on Script to Program Evolution (STOP2009), Genoa, Italy, July, 2009.

Abstract

Gradual typing is a framework to combine static and dynamic typing in a single programming language. In this paper, we develop a gradual type system for class-based object-oriented languages with generics. We introduce a special type to denote dynamically typed parts of a program; unlike dynamic types introduced to C# 4.0, however, our type system allows for more seamless integration of dynamically and statically typed code.

We formalize a gradual type system for Featherweight GJ with a semantics given by a translation that inserts explicit run-time checks. The type system guarantees that statically typed parts of a program do not go wrong, even if it includes dynamically typed parts. We also describe a basic implementation scheme for Java and report preliminary performance evaluation.

File(s)