Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands

First-class functions dramatically increase expressiveness,
at the expense of static guarantees.
In ALGOL or PASCAL, functions could be passed as arguments
but never escape their defining scope.
Therefore, function arguments could serve as temporary access
tokens or capabilities, enabling callees to perform some
action, but only for the duration of the call.
In modern languages, such programming patterns are
no longer available.

The central thrust of this paper is to re-introduce
second-class functions and other values alongside
first-class entities in modern languages.
We formalize second-class values with stack-bounded
lifetimes as an extension to simply-typed $\lambda$ calculus,
and for richer type systems such as F$_{<:}$ and systems
with path-dependent types.
We generalize the binary first- vs second-class
distinction to arbitrary privilege lattices, with the
underlying type lattice as a special case. In this setting,
abstract types naturally enable privilege parametricity.
We prove type soundness and lifetime properties in Coq.

We implement our system as an extension of Scala,
and present several case studies.
First, we modify the Scala Collections library and add
privilege annotations to all higher-order functions.
Privilege parametricity is key to retain the high degree
of code-reuse between sequential and parallel as well as
lazy and eager collections.
Second, we use scoped capabilities to introduce a model
of checked exceptions in the Scala library, with
only few changes to the code.
Third, we employ second-class capabilities for memory
safety in a region-based off-heap memory library.