At previous NJPLS meetings, we have presented talks on the design of the Moby programming language. Since the last of these, we have been hard at work on an implementation. In this talk I'll discuss the state of the Moby language design and implementation.
Parameterized object types are a useful addition to typed object-oriented languages, allowing full static type-checking of container objects without sacrificing expressiveness. Subtyping for parameterized object types is normally restricted, to ensure type safety, and attempts to weaken these restrictions lead to possible runtime type errors (as with the Java treatment of subtyping for array types). Cardelli suggested polarized subtyping as a safe way of extending subtyping for parameterized types. Steffen investigated the metatheory of polarized subtyping. Duggan and Compagnoni proposed polarized object type constructors as a variation of this approach with better metatheoretic properties. Hosoya and Pierce have worked on a system with similar properties.
In this talk I will review the approach of polarized object type constructors and discuss the problems with combining polarized subtyping with interface containment. I will then describe a new polarity that allows statically unsafe but dynamically safe covariant subtyping, that provides an avenue around these problems. This approach is particularly appropriate for Java, and the talk will emphasize the application to parameterized types in Java.
This talk will give an overview of the infrastructure, and then give a more detailed presentation of the HPL-PD architecture, including its relationship to new processors expected to emerge over the next few years.
Trimaran, http://www.trimaran.org, is a collaborative effort between the CAR group at Hewlett Packard Laboratories, the IMPACT project at the University of Illinois, and the ReaCT-ILP project at New York University.
Type systems and flow logic are two popular frameworks for specifying program analyses. While these frameworks seem rather different on the surface, both describe the "plumbing" of a program, and recent work has uncovered deep connections between them. In the case of common monovariant flow analyses, corresponding type systems have been established by Palsberg & O'Keefe and by Heintze. In the case of argument-based polyvariant flow analyses, Palsberg & Pavlopoulou have shown a correspondence to a type system with union and intersection types.
If type and flow systems really encode similar information, "round-trip" translations from flow analyses to type derivations and back (or from type derivations to flow analyses and back) should not lose precision. Rather, they should be "faithful" in the sense that doing a roundtrip acts as the identity for "canonical" forms, and otherwise canonicalizes. Palsberg & Pavlopoulou's correspondence is not faithful, but we develop a modified flow/type correspondence that is. This result is achieved by augmenting union and intersection types with component labels; these serve as witnesses for the existential quantifiers in the rules for subtyping (and so they can be justified independently of the flow/type correspondence).
Additionally, our flow/type correspondence solves several open problems posed by Palsberg & Pavlopoulou. By specifying our flow system in the style of Nielson & Nielson, we are able to express call-string based polyvariance (such as kCFA) in addition to argument based polyvariance, and to establish a subject reduction property (which can be lifted to the type setting). And our correspondence is designed with the aim of letting "flows have it their way" rather than letting "types have it their way".
Anindya Banerjee / ab@cs.stevens-tech.edu