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. This fragment assumes the absence of so
called
handle errors that violate the single assignment
assumption of Lambda(fut)'s handled future-construct.
Finally, we present a linear type system for Lambda(fut)
by which to prove the absence of handle errors. Our
system is rich enough to type definitions
of the above mentioned concurrency abstractions. Consequently,
these cannot be corrupted in any (not necessarily linearly)
well-typed context.
Revised version from FroCoS'05.