Various concurrency primitives have been added to sequential programming languages, in order to turn them concurrent. Prominent examples are concurrent buffers for Haskell, channels in Concurrent ML, joins in JoCaml, and handled futures in Alice ML. Even though one might conjecture that all these primitives provide the same expressiveness, proving this equivalence is an open challenge in the area of program semantics. In this paper, we establish a first instance of this conjecture. We show that concurrent buffers can be encoded in the lambda calculus with futures underlying Alice ML. Our correctness proof results from a systematic method, based on observational semantics with respect to may and must convergence.
The need for flexible forms of serialisation arises under many circumstances, e.g. for doing high-level inter-process communication or to achieve persistence. Many languages, including variants of ML, thus offer pickling as a system service, but usually in a both unsafe and inexpressive manner, so that its use is discouraged. In contrast, safe generic pickling plays a central role in the design and implementation of Alice ML: components are defined as pickles, and modules can be exchanged between processes using pickling. For that purpose, pickling has to be higher-order and typed (HOT), i.e. embrace code mobility and involve runtime type checks for safety. We show how HOT pickling can be realised with a modular architecture consisting of multiple abstraction layers for separating concerns, and how both language and implementation benefit from a design consistently based on pickling.
We introduce a new lambda calculus with futures, Lambda(fut), that models the operational semantics of concurrent statically typed functional programming languages with mixed eager and lazy threads such as Alice ML, a concurrent extension of Standard ML. Lambda(fut) is a minimalist extension of the call-by-value lambda-calculus that is sufficiently expressive to define and combine a variety of standard concurrency abstractions, such as channels, semaphores, and ports. Despite its minimality, the basic machinery of Lambda(fut) is sufficiently powerful to support explicit recursion and call-by-need evaluation. We present a static type system for Lambda(fut) and distinguish a fragment of Lambda(fut) that we prove to be uniformly confluent. This result confirms our intuition that reference cells are the sole source of indeterminism.
Despite its powerful module system, ML has not yet evolved for the modern world of dynamic and open modular programming, to which more primitive languages have adapted better so far. We present the design and semantics of a simple yet expressive first-class component system for ML. It provides dynamic linking in a type-safe and type-flexible manner, and allows selective execution in sandboxes. The system is defined solely by reduction to higher-order modules plus an extension with simple module-level dynamics, which we call packages. To represent components outside processes we employ generic pickling. We give a module calculus formalising the semantics of packages and pickling.
ML modules provide hierarchical namespace management, as well as fine-grained control over the propagation of type information, but they do not allow modules to be broken up into separately compilable, mutually recursive components. Mixin modules facilitate recursive linking of separately compiled components, but they are not hierarchically composable and typically do not support type abstraction. We synthesize the complementary advantages of these two mechanisms in MixML. A MixML module is like an ML structure with some components specified but not defined unifing the ML structure and signature languages into one. MixML seamlessly integrates hierarchical composition, translucent MLstyle data abstraction, and mixin-style recursive linking.Tthe design of MixML is minimalist emphasizing how all the interesting features of the ML module system can be understood simply as stylized uses of a small set of orthogonal underlying constructs, with mixin composition playing a central role.