Also see the GJ home page and Pizza home page.
A brilliant exposition of generics. By far the best book on the topic, it provides a crystal clear tutorial that starts with the basics and ends leaving the reader with a deep understanding of both the use and design of generics.
— Gilad Bracha, Java Generics Lead, Sun Microsystems
Faith and evolution provide complementary--and sometimes conflicting--models of the world, and they also can model the adoption of programming languages. Adherents of competing paradigms, such as functional and object-oriented programming, often appear motivated by faith. Families of related languages, such as C, C++, Java, and C#, may arise from pressures of evolution. As designers of languages, adoption rates provide us with scientific data, but the belief that elegant designs are better is a matter of faith.
This talk traces one concept, second-order quantification, from its inception in the symbolic logic of Frege through to the generic features introduced in Java 5, touching on aspects of faith and evolution. The remarkable correspondence between natural deduction and functional programming informed the design of type classes in Haskell. Generics in Java evolved directly from Haskell type classes, and are designed to support evolution from legacy code to generic code. Links, a successor to Haskell aimed at AJAX-style three-tier web applications, aims to reconcile some of the conflict between dynamic and static approaches to typing.
Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy.
Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations.
As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.
This is the conference version of the TOPLAS paper.
Short abstract: We present GJ, a design that extends the Java programming language with generic types and methods. GJ increases expressiveness and safety: code utilizing generic libraries is no longer buried under a plethora of casts. GJ is designed to be fully backwards compatible with the current Java language, which simplifies the transition from non-generic to generic programming.
Long abstract: The best way to program is to get someone else to do it for you: exploit a reusable library. Many classes, especially reusable ones, are best thought of as generic; for instance, a list is generic in its element type. Java 1.1.6 comes with a Collections Library, including lists, similar to the Standard Template Library for C++. Such classes are easy to define in Java, but not so easy to use. The definer implements a class List where the elements are of type Object. The user has to remember what kind of list it is, and to add casts from Object to the element type where appropriate.
GJ extends Java with generic types. Typing is more precise: one may replace the uninformative List by the more precise, say, List<String>. And there is less to type: no extra casts to insert. Many common errors are caught by the compiler rather than left lurking until run-time. The mechanism looks like templates in C++, but has greater power (you can specify what interface a type should implement) and fewer drawbacks (no risk of code bloat).
GJ contains Java as a subset, and the GJ compiler may be used as a Java compiler. GJ compiles into Java bytecodes, so it runs wherever Java runs. GJ is fully forward and backward compatible: new GJ code may use legacy Java libraries; and legacy Java code may be linked with new GJ libraries. Legacy Java libraries may be retrofitted with GJ types, even if the source is unavailable; in particular, the Java Collections Library has been augmented with generic types. The GJ compiler is itself written in GJ, and is freely available over the web.
GJ is joint work with Martin Odersky at the University of South Australia, and Gilad Bracha and Dave Stoutamire at Sun. GJ was designed so that it could be incorporated into a future Java release, although whether this will happen is unclear. Compatibility with GJ was a design consideration for the new Java Collections Libary.
The Expression Problem is a new name for an old problem. The goal is to define a datatype by cases, where one can add new cases to the datatype and new functions over the datatype, without recompiling existing code, and while retaining static type safety (e.g., no casts). For the concrete example, we take expressions as the data type, begin with one case (constants) and one function (evaluators), then add one more construct (plus) and one more function (conversion to a string).
[This note was widely cited but never published.]
We present GJ, a design that extends the Java programming language with generic types and methods. These are both explained and implemented by translation into the unextended language. The translation closely mimics the way generics are emulated by programmers: it erases all type parameters, maps type variables to their bounds, and inserts casts where needed. Some subtleties of the translation are caused by the handling of overriding.
GJ increases expressiveness and safety: code utilizing generic libraries is no longer buried under a plethora of casts, and the corresponding casts inserted by the translation are guaranteed to not fail.
GJ is designed to be fully backwards compatible with the current Java language, which simplifies the transition from non-generic to generic programming. In particular, one can retrofit existing library classes with generic interfaces without changing their code.
An implementation of GJ has been written in GJ, and is freely available on the web.
This tutorial introduces the concepts of GJ by example.
This specification defines GJ in rigorous detail.
Functional programmers and reuse engineers dine at the same table. Delicacies like type abstraction and higher-order functions are meat and potatoes for those who need to reuse code parameterised by types and operations.
The talk will start with a review of modern functional languages. Isolation has given way to systems that interact with C and COM components. Code quality can rival C. Functional programs deliver calls in Brussels, route planes through Paris, and play CDs over networks at Cornell.
The talk will then describe Pizza, an attempt to make functional ideas accessible to a wider community by embedding them in Java. Pizza contains Java as a subset, so its easy to learn, and it compiles to the Java Virtual Machine, so it runs anywhere Java runs, including web browsers. We will focus on how Pizza is designed to add parametric types on top of existing Java libraries, enhancing reuse.
Applications of functional languages have been described elsewhere; this paper describes salient features of the latest version of Pizza.
Parametric types and virtual types have recently been proposed as extensions to Java to support genericity. In this paper we examine both in order to investigate the strengths and weaknesses of each. We suggest a variant of virtual types which has similar expressiveness, but supports safe static type checking. This results in a language in which both parametric types and virtual types are well-integrated, and which is statically type-safe.
Pizza is a strict superset of Java that incorporates three ideas from the academic community:
