The purpose of the library is to provide mechanisms for reasoning about state based dynamic system. Due to a separation of concerns, the library allows to reason about such system purely mathematically, without any dependency on the actual representation of the state, or how the dynamism is handled. Putting it more simple, the library allows to reason about mathematical objects, whose value changes with time. Such objects, are usually model some complex systems with a hidden state, that can be only observed. This kind of systems is hard and practically impossible to describe using inductive types. We reify such systems with coinduction. The library defines two main coinductive types:
future type is dual of the option type (a co-option), and
stream is a dual of the list (co-list).
A value of type
future is an object, with some observable state, that is not yet defined. We know, that it might happen, but it is not guaranteed. The
future can be defined only once. Once it is defined, it cannot be changed. Basically, the time line of the
future object is separated into two phases: on a first phase the value of the object is undefined, and on the second it is defined and fixed. Both phases can be empty, i.e., an object can be brought into life with a defined value, and an undefined future, might be never defined.
A value of type
stream is an infinite sequence of finite values. More precisely, a stream can be viewed as an object, whose value varies in time.
The library can be also seen as a common denominator between different async libraries and methods, e.g., lwt, async, threads, forthcoming effective programming in multicore OCaml, etc. For example, the
future are quite similar to the
Lwt library and to the
Deferred.t of the
Async library. There are few differences, however. The
future library tries to separate concerns, so unlike
Async libraries, future can't fail. In other words, if a computation that computes the
future fails, that just means, that this particular future has never occurred. If a user wants to represent a future value, that can fail or succeed, that he is welcome to use sum types, e.g.,
('a,'b) Result.t future. The same is true for the async library.
Notion of time
The future library handles time in a special way. The notion of physical time is replaced with the notion of order. We consider only the precedence of events. There is no notion of simultaneity built into the model of the library. Every event occurs in its own separate time slot, i.e., all events are serialized in the time.
That is not to say, that simultaneous events are not representable. The library just allows a user, to engineer its own timescale and define, what is simultaneous and what is not. For example, a clock timer can be represented as a stream of seconds, and everything that occurs after the start of the
n'th second, but before the start of the
n+1'th second, is simultaneous.
Since the internal state of the dynamic system is usually impossible to represent, it is modeled by a notion of primitive signals and promises. When a future is created a corresponding promise is made. The system, that models the dynamic system is responsible to fulfill the promise. A signal is akin to the promise, with only difference, that it can (and should) be fulfilled, or signaled, more than once.
The use of promises and signals is totally under a user control and is separated from the rest of the library. They can be signaled from event loops, such as Lwt or Async main loops, or from a window system event loop. The only requirement, is that this calls should be serialized, if it is possible that they are made from different threads.
A common way to bind
Lwt thread with
Future is to use
on_success function (or
upon function for
let future_of_thread t = let future,promise = Future.create () in Lwt.on_success t (Promise.fulfill promise); future
module Applicable : sig ... end
module Variadic : sig ... end
module Future : sig ... end
Future is an object whose value will be decided somewhere in the future, if that future has occurred.
module Promise : sig ... end
An promise to provide a value in a future.
module Stream : sig ... end
A stream of elements.
module Signal : sig ... end
A handler to produce elements in streams.