Alice Project


________ Overview ____________________________________________________

A future is a place-holder for the undetermined result of a (concurrent) computation. Once the computation delivers a result, the associated future is eliminated by globally replacing it with the result value. That value may be a future on its own.

Whenever a future is requested by a concurrent computation, i.e. it tries to access its value, that computation automatically synchronizes on the future by blocking until it becomes determined or failed.

There are four kinds of futures:

________ Concurrency _________________________________________________

A concurrent future is created by the expression

spawn exp

which evaluates the expression exp in a new thread and returns immediately with a future of its result. When the expression has been evaluated, the future is globally replaced by the result. We speak of functional threads. See the discussion on failed futures below for the treatment of possible error conditions.

Note: The presence of concurrency has subtle implications on the semantics of pattern matching.


The following expression creates a table and concurrently fills it with the results of function f. Each entry becomes available as soon as its calculation terminates:

Vector.tabulate (30, fn i => spawn f i)

Syntactic sugar

A derived form is provided for defining functions that always evaluate in separate threads:

fun spawn f x y = exp

An application f a b will spawn a new thread for evaluation. See below for a precise definition of this derived form.

________ Laziness ____________________________________________________

An expression can be marked as lazy:

lazy exp

A lazy expression immediately evaluates to a lazy future of the result of exp. As soon as a thread requests the future, the computation is initiated in a new thread. The lazy future is replaced by a concurrent future and evaluation proceeds similar to spawn. In particular, failure is handled consistently.


Lazy futures enable full support for the whole range of lazy programming techniques. For example, the following function generates an infinite lazy stream of integers:

fun enum n = lazy n :: enum (n+1)

Syntactic sugar

Analogously to spawn, a derived form is provided for defining lazy functions:

fun lazy f x y = exp

See below for a precise definition of this derived form. It allows convenient formulation of lazy functions. For example, a lazy variant of the map function on lists can be written

fun lazy mapz f   []    = nil
       | mapz f (x::xs) = f x :: mapz f xs

This formulation is equivalent to

fun mapz f xs = lazy (case xs of
                           []   => nil
                        | x::xs => f x :: mapz f xs)

________ Promises ____________________________________________________

Promises are explicit handles for futures. A promise is created through the polymorphic library function Promise.promise:

val p = Promise.promise ()

Associated with every promise is a future. Creating a new promise also creates a fresh future. The future can be extracted as

val f = Promise.future p

A promised future is eliminated explicitly by applying

Promise.fulfill (p, v)

to the corresponding promise, which globally replaces the future with the value v.

Note: Promises may be thought of as single-assignment references that allow dereferencing prior to assignment, yielding a future. The operations promise, future and fulfill correspond to ref, ! and :=, respectively.


Promises essentially represent a more structured form of "logic variables" as found in logic programming languages. Their presence allows application of diverse idioms from concurrent logic programming to ML. Examples can be found in the documentation of the Promise structure.

________ Failed futures ______________________________________________

If the computation associated with a concurrent or lazy future terminates with an exception, that future cannot be eliminated. Instead, it turns into a failed future. Promised futures can be failed explicitly by means of the function. Requesting a failed future does not block. Instead, any attempt to request a failed future will re-raise the exception that was the cause of the failure.

Another error condition is the attempt to replace a future with itself. This may happen if a recursive spawn or lazy expression is unfounded, or if a promise is fulfilled with its own future. In all of these cases, the future will be failed with the special exception Future.Cyclic.

________ Requesting a future _________________________________________

The future semantics implies implicit data-flow synchronisation, which enables concurrent programming on a high level of abstraction.

A future is requested if it is used as an argument to a strict operation. The following operations are strict (note that futures can appear on the module level):

Note however, that selecting items from a structure using longids is non-strict.

If a future is requested by a thread, that thread blocks until the future has been replaced by a non-future value (or a failed future). After the value has been determined, the thread proceeds. The only exception are failed futures, which do not block.

Requesting a lazy future triggers initiation of the corresponding computation. The future is replaced by a concurrent future of the computation's result. The requesting thread blocks until the result is determined.

Requesting a promised future will block at least until a fulfill operation has been applied to the corresponding promise. Blocking continues if the promise is fulfilled with another future.

Requesting a failed future never blocks. Instead, the exception that was the cause of the failure will be re-raised.

Structural operations that are strict (i.e., pattern matching, op= and pickling) traverse all values in a depth-first left-to-right order. Futures are requested in that order. If traversal is terminated early, the remaining futures are not requested. Early termination occurs if a future is failed, upon a mismatch (pattern matching), if two partial values are not equal (op=), or if part of a value is sited (pickling). For unpacking it is unspecified, how much of the respective signatures is requested.

________ Threads and state ___________________________________________

To deal with state in a thread-safe way, the structure Ref provides an atomic exchange operation for references:

val exchange : 'a ref * 'a -> 'a

With exchange, the content of a cell can be replaced by a new value. The old value is returned. The exchange operation is atomic, and can thus be used for synchronisation. As an example, here is the implementation of a generic lock generator:

fun lock () =
	val r = ref ()
	fn f => fn x =>
	    val new = Promise.promise ()
	    val old = (r, Promise.future new)
	    await old;
	    f x before
	    Promise.fulfill (new, ()))

The library structure Lock implements locks this way.

________ Modules _____________________________________________________

Modules can be futures as well. See Laziness and Concurrency for modules.

________ Library support _____________________________________________

The following library modules provide functionality relevant for programming with futures, promises and concurrent threads:

ByNeed is a functor that allows creation of lazy futures for modules. Lazy modules are also at the core of the semantics of components.

________ Syntax summary ______________________________________________

exp ::= ...
lazy exp lazy
spawn exp concurrent
fvalbind ::= <lazy | spawn> (m,n≥1) (*)
   <op> vid atpat11 ... atpat1n <: ty1> = exp1
| <op> vid atpat21 ... atpat2n <: ty2> = exp2
| ...
| <op> vid atpatm1 ... atpatmn <: tym> = expm
<and fvalbind>

Derived forms

<lazy | spawn>
   <opvid atpat11 ... atpat1n <: ty1= exp1
| <opvid atpat21 ... atpat2n <: ty2= exp2
|    ...
| <opvid atpatm1 ... atpatmn <: tym= expm
<and fvalbind>
<opvid = fn vid1 => ... fn vidn =>
<lazy | spawncase (vid1,...,vidn) of
   (atpat11,...,atpat1n) => exp1 <: ty1>
| (atpat21,...,atpat2n) => exp2 <: ty2>
|    ...
| (atpatm1,...,atpatmn) => expm <: tym>
<and fvalbind>

vid1,...,vidn are distinct and new.

last modified 2004/12/20 21:56