Type-preserving compilation of (most of) FGJ into DOT

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not enough to declare a particular subset of the language as sound. While a few examples of Scala snippets have been manually translated into DOT, no systematic compilation scheme has been presented so far. In this report we take advantage of the fact that the Featherweight Generic Java (FGJ) calculus can be seen as a subset of Scala (you just have to squint a little bit!) and present a compilation scheme from cast-less FGJ into DOT as well as a proof that a well-typed cast-less FGJ program compiles down to a well-typed DOT term. Due to limitations in DOT subtyping rules, this requires imposing one limitation on our source program: the type parameters of the base types of a class can never refer back to the class itself (this excludes class C extends B[C] as well as class D extends B[E]; class E extends D). While this result is not especially interesting by itself given that FGJ is already known to be sound, it is a first step towards establishing soundness for larger subsets of Scala like the Pathless Scala calculus, the author plans to pursue this in his thesis (currently under preparation) which will also include the content of this report. It also clearly illustrates limitations in DOT that future work may wish to focus on.

Object-oriented pattern matching

Burak Emir

Pattern matching is a programming language construct considered essential in functional programming. Its purpose is to inspect and decompose data. Instead, object-oriented programming languages do not have a dedicated construct for this purpose. A possible reason for this is that pattern matching is useful when data is defined separately from operations on the data – a scenario that clashes with the object-oriented motto of grouping data and operations. However, programmers are frequently confronted with situations where there is no alternative to expressing data and operations separately – because most data is neither stored in nor does it originate from an object-oriented context. Consequently, object-oriented programmers, too, are in need for elegant and concise solutions to the problem of decomposing data. To this end, we propose a built-in pattern matching construct compatible with object-oriented programming. We claim that it leads to more concise and readable code than standard object-oriented approaches. A pattern in our approach is any computable way of testing and deconstructing an object and binding relevant parts to local names. We introduce pattern matching in two variants, case classes and extractors. We compare the readability, extensibility and performance of built-in pattern matching in these two variants with standard decomposition techniques. It turns out that standard object-oriented approaches to decomposing data are not extensible. Case classes, which have been studied before, require a low notational overhead, but expose their representation, making them hard to change later. The novel extractor mechanism offers loose coupling and extensibility, but comes with a performance overhead. We present a formalization of object-oriented pattern matching with extractors. This is done by giving definitions and proving standard properties for a calculus that provides pattern matching as described before. We then give a formal, optimizing translation from the calculus including pattern matching to its fragment without pattern matching, and prove it correct. Finally, we consider non-obvious interactions between the pattern matching and parametric polymorphism. We review the technique of generalized algebraic data types from functional programming, and show how it can be carried over to the object-oriented style. The main tool is the extension of the type system with subtype constraints, which leads to a very expressive metatheory. Through this theory, we are able to express patterns that operate on existentially quantified types purely by universally quantified extractors.

EPFL2007

Foundations for SCALA

Vincent Cremet

SCALA is an attractive programming language because it is both very expressive and statically strongly typed. This marriage against nature comes at the price of a certain complexity in the language constructs and the static analysis. This complexity makes type safety unclear. The goal of this thesis is to initiate a rigorous and formal process of validation of the SCALA type system. The correctness of a type system can only be established in relation to a formal description of a program execution. The first contribution of this thesis is the definition of a formal semantics for SCALA, by translation in a minimal class-based calculus. SCALA offers two means for expressing type abstraction: type parameters and type members, also called virtual types. Virtual types seem more primitive since they allow to encode type parameters whereas the existence of a reverse encoding is not clear. The soundness of virtual types has been the object of a long debate in the community; they are now commonly believed to be safe, but at this time, there exists no formal argument that would confirm this belief. The second contribution of this thesis is to provide a formal proof of type safety for virtual types.

EPFL2006

Type-Safe Prototype-Based Component Evolution

Matthias Zenger

Component-based programming is currently carried out using mainstream object-oriented languages. These languages have to be used in a highly disciplined way to guarantee flexible component composition and extensibility. This paper investigates abstractions for component-oriented programming on the programming language level. We propose a simple prototype-based model for first-class components on top of a class-based object-oriented language. The model is formalized as an extension of Featherweight Java. Our calculus includes a minimal set of primitives to dynamically build, extend, and compose software components, while supporting features like explicit context dependencies, late composition, unanticipated component extensibility, and strong encapsulation. We present a type system for our calculus that ensures type-safe component definition, composition, and evolution.

2002

Object-oriented pattern matching

Burak Emir

EPFL2007