package bap-future

Future library.

Overview

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 and stream. The 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.t in 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 Lwt or 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.

Main-loop

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 Async's Deferred):

let future_of_thread t =
  let future,promise = Future.create () in
  Lwt.on_success t (Promise.fulfill promise);
  future