How are Futures described in terms of category theory?

Question

Is there a useful description of futures or promises in terms of category theory? In particular, what could the categorical dual of Future be?

Answer 1

As it happens, I'm writing a paper about this now. IMO, a good way to think about futures or promises is in terms of the Curry-Howard correspondence for temporal logic.

Basically, the idea behind futures is that it is a data structure representing a computation that is in progress, and upon which you can synchronize. In terms of temporal logic, this is the eventually operator $\Diamond A$. This has a monadic structure: $$ \begin{array}{lcl} \mathrm{return} & : & A \to \Diamond A \\ \mathrm{bind} & : & (A \to \Diamond{B}) \to \Diamond{A} \to \Diamond{B} \end{array} $$ in which the $\mathrm{return}$ operation spawns a process that immediately returns its argument, and $\mathrm{bind}$ creates a new process which waits for $a$'s value, applies $f$ to that value, and then waits for the $B$-value before returning. The Promises/A proposal for CommonJS calls the monadic bind operation then, and Scala 2.10 just gives it the standard monadic interface.

The dual to the eventually operator $\Diamond{A}$ is the always operator $\Box{A}$ of temporal logic, which says that at every instant, you get an $A$. When you pass from a Kripke semantics of temporal logic (where you just model provability) to a categorial semantics of a $\lambda$-calculus (where you model lambda-terms/proofs also), it turns out there are actually multiple ways to do this.

The simplest thing you can do is to take $\Box{A} \triangleq A$, on the grounds that once you have an $A$, you always have it. This works, but is kind of boring, IMO. :)

The most natural (IMO) thing to do is to take $\Box{A} \triangleq \mathsf{Stream}\;A$, which permits you to get a (potentially different) $A$ at each instant. Then, you can see the comonadic style of functional reactive programming (FRP) (first proposed by Tarmo Uustalu and Varmo Vene) as the dual to monadic style of programming with futures.

However, the comonadic $\lambda$-calculus as they suggest, despite its elegance, causes a serious loss of expressiveness relative to programming explicitly with streams, since the category of free coalgebras they use turns out to have too few global elements to denote many interesting programs, especially fixed points.

Nick Benton and I have argued for programming explicitly with streams in our paper Ultrametric Semantics of Reactive Programs. Subsequently, Alan Jeffrey suggested using LTL as a type system in his paper LTL types FRP, an observation that Wolfgang Jeltsch also made in his paper Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming.

The difference between the view Nick and I take, and the one that Alan and Wolfgang take is best understood (IMO) by comparing the construction given in Birkedal et al.'s First steps in synthetic guarded domain theory: step-indexing in the topos of trees with Alan's paper. The topos of trees (presheaves over the natural numbers ordered by size) is very similar to category of ultrametric spaces Nick and I used, but much easier to compare with Alan's category (presheaves over a discrete category of time), since these are both presheaf categories.

If you're interested in futures specifically for concurrency, then it might be a better idea to look at CTL rather than LTL, though. AFAIK, that's presently unexplored territory!

EDIT: here's a link to the draft. The paper is mostly about implementing typed FRP, so the language is synchronous. But most of the discussion of futures/events in section 3.3 should basically apply to truly concurrent languages as well.