Gradual Pluggable Typing in Java

Abstract

Gradual typing provides the ability to safely mix untyped or dynamically typed code with statically typed code while maintaining, within the statically typed portion, the guarantees claimed by the static typing. It is motivated by the idea that different amounts of typing are valuable at different times during a software projects development. Less typing is useful at the prototyping stage, where requirements change frequently, and rapid development is important. More typing is useful in more mature projects where maintenance, documentation, and correctness become critically important. Gradual aims to enable a project to gradually move from one side of this spectrum to the other.

Pluggable typing and pluggable typing frameworks aim to allow a language to support many different type systems, that can be developed by type system designers and plugged into the existing compiler infrastructure. The Checker Framework is built on the OpenJDK➋ Java compiler, and provides a framework to develop additional type systems that can be applied to Java code. It has been tested and proven using many other type systems. However, not all code will adopt all type systems, so a developer who wishes to check their project with a given type system may still link against other components that are not checked with that type system. Additionally, a developer may wish to adopt a new type system, but be unwilling to spend the effort necessary to annotate all the existing code for the new type system.

The gradual extension to the Checker Framework aims to improve type safety of partially applied Checker Framework type systems, using gradual typing techniques. A prototype was built, and the gradual nullness type system was designed to prove it.

Defining the checked-unchecked boundary is crucial. Even though the use case is limited to individual files being either entirely annotated or entirely unannotated, because Java is an object-oriented language with inheritance, many different boundary conditions present themselves. This work analyses each boundary condition in detail, and presents options for runtime tests to ensure that values crossing the boundary meet the static type requirements on the other side. The nature of the tests, and the method of passing the static type to the runtime environment is discussed.

This work presents the design of the prototype, implemented in the Checker Framework and OpenJDK➋. It discusses the design of the OpenJDK➋ compiler, the Checker Framework, and how they work together. It demonstrates how the abstract syntax tree can be modified in order to effect insertion of the runtime tests. It discusses the specific implementation details needed to implement each boundary condition runtime test in Java.

An evaluation of the prototype is completed looking at correctness, both through a set of synthetic tests, and by inserting artificial errors into an existing real world program; performance, by running configurations of real world programs designed to model the motivating examples; and applicability, by comparing the gradual framework with other options for improving type safety in partially annotated programs.

Related work on both gradual typing and pluggable typing are discussed. Final remarks and future work concludes the work.