Spores, Formally | EPFL Graph Search

Functional programming (FP) is regularly touted as the way forward for bringing parallel, concurrent, and distributed programming to the mainstream. The popularity of the rationale behind this viewpoint (immutable data transformed by function application) has even lead to a number of object-oriented (OO) programming languages adopting functional features such as lambdas (functions) and thereby function closures. However, despite this established viewpoint of FP as an enabler, reliably distributing function closures over a network, or using them in concurrent environments nonetheless remains a challenge across FP and OO languages. This paper takes a step towards more principled distributed and concurrent programming by introducing a new closure-like abstraction and type system, called spores, that can guarantee closures to be serializable, thread-safe, or even have general, custom user-defined properties. Crucially, our system is based on the principle of encoding type information corresponding to captured variables in the type of a spore. We prove our type system sound, implement our approach for Scala, evaluate its practicality through an small empirical study, and show the power of these guarantees through a case analysis of real-world distributed and concurrent frameworks that this safe foundation for migratable closures facilitates. In this report, we present the detailed soundness proofs of spores.

Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution

Philipp Haller, Martin Odersky

2014

Programming language abstractions for mobile code

Stéphane Micheloud

Scala is a general-purpose programming language developed at EPFL. It combines the most important concepts found in object-oriented and functional languages. Scala is a statically typed language; in particular it features an advanced type system and supports local type inference. Furthermore it integrates well with the Java and .net platforms: their libraries are accessible without glue code and the Scala compiler generates code for both execution environments. The Scala programming language has several features that make it desirable as a language for distributed application programming. In particular, it supports first-class functions which are useful in relation with the notions of distributed scope and code mobility. In that context, the missing support for run-time types is one important drawback of the Java run-time environment as a target platform. This thesis focuses on the realisation of a new concept combining essential notions from the functional and distributed programming and implying the extension of the notion of lexical scoping to the distributed context. In short, we claim that the notion of lambda abstraction provides an elegant way for dealing with the dynamic rebinding of local references in a distributed execution environment. The key ideas exposed in this research work have been implemented in our Scala compiler. This helped us to evaluate the used techniques, in particular their impact on the reliability and the performance of distributed programs. So far, most research works related to the present subject have focused on functional programming languages, in particular on the ML language family.

EPFL2009

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

Object-oriented pattern matching

Burak Emir

EPFL2007