<p>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 <a href="http://en.wikipedia.org/wiki/Temporal_logic">temporal logic</a>. </p>

<p>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} &amp; : &amp; A \to \Diamond A \\
\mathrm{bind} &amp; : &amp; (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 <a href="http://wiki.commonjs.org/wiki/Promises/A">Promises/A proposal for CommonJS</a> calls the monadic bind  operation <code>then</code>, and <a href="http://docs.scala-lang.org/sips/pending/futures-promises.html">Scala 2.10 just gives it the standard monadic interface</a>. </p>

<p>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.</p>

<p>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. :) </p>

<p>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 <a href="http://cs.ioc.ee/~tarmo/papers/essence.pdf">Tarmo Uustalu and Varmo Vene</a>) as the dual to monadic style of programming with futures. </p>

<p>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.</p>

<p>Nick Benton and I have argued for programming explicitly with streams in our paper <a href="http://www.cs.cmu.edu/~neelk/frp-lics11.pdf"><em>Ultrametric Semantics of Reactive Programs</em></a>. Subsequently, Alan Jeffrey suggested using LTL as a type system in his paper <a href="http://ect.bell-labs.com/who/ajeffrey/papers/plpv12.pdf"><em>LTL types FRP</em></a>, an observation that Wolfgang Jeltsch also made in his paper <a href="http://www.ioc.ee/~wolfgang/research/mfps-2012-paper.pdf"><em>Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming</em></a>. </p>

<p>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 <a href="http://www.itu.dk/~birkedal/papers/sgdt-journal.pdf"><em>First steps in synthetic guarded domain theory: step-indexing in the topos of trees</em></a> 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. </p>

<p>If you're interested in futures specifically for concurrency, then it might be a better idea to look at <a href="http://en.wikipedia.org/wiki/Computation_tree_logic">CTL</a> rather than LTL, though. AFAIK, that's presently unexplored territory! </p>

<p>EDIT: here's a <a href="http://www.mpi-sws.org/~neelk/simple-frp.pdf">link to the draft</a>. 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. </p>

CC BY-SA 3.0
2012-11-12T13:43:32.463Z
I'd love to get a copy of that when you've finished it.
Dave Clarke
CC BY-SA 3.0
2012-11-12T19:25:38.473Z
It seems that this loses an important characteristic of futures: once a value is obtained, it can't change. I'd try to express it by taking $A \to \Box A$ as an axiom, but this is not what we want if $\Box$ means a stream... And I'd also like a copy of the paper when it's done :)
Alexey Romanov
CC BY-SA 3.0
2013-12-05T19:50:48.290Z
I recently read that the Scala type `Try[T]` and `Future[T]` are dual, but I have not quite understood what this means / in what sense.
Giorgio
CC BY-SA 3.0
2012-11-12T08:04:10.023Z
2012-11-14T13:21:50.867Z
2012-11-14T13:21:50.867Z
Neel Krishnaswami
<p>Is there a useful description of <a href="http://en.wikipedia.org/wiki/Futures_and_promises">futures or promises</a> in terms of category theory? In particular, what could the categorical dual of Future be?</p>

<pl.programming-languages><ct.category-theory><concurrency>
How are Futures described in terms of category theory?
Alexey Romanov
# How are Futures described in terms of category theory?

(Asked by: username_0 on 2012-11-12)

Is there a useful description of [futures or promises](http://en.wikipedia.org/wiki/Futures_and_promises) in terms of category theory? In particular, what could the categorical dual of Future be?

**Tags:** pl.programming-languages, ct.category-theory, concurrency

---

## 1 answers

### Answer by username_1 on 2012-11-12. Score: 25 | Accepted answer

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](http://en.wikipedia.org/wiki/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](http://wiki.commonjs.org/wiki/Promises/A) calls the monadic bind operation `then`, and [Scala 2.10 just gives it the standard monadic interface](http://docs.scala-lang.org/sips/pending/futures-promises.html).

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](http://cs.ioc.ee/~tarmo/papers/essence.pdf)) 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*](http://www.cs.cmu.edu/~neelk/frp-lics11.pdf). Subsequently, Alan Jeffrey suggested using LTL as a type system in his paper [*LTL types FRP*](http://ect.bell-labs.com/who/ajeffrey/papers/plpv12.pdf), an observation that Wolfgang Jeltsch also made in his paper [*Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming*](http://www.ioc.ee/~wolfgang/research/mfps-2012-paper.pdf).

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*](http://www.itu.dk/~birkedal/papers/sgdt-journal.pdf) 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](http://en.wikipedia.org/wiki/Computation_tree_logic) rather than LTL, though. AFAIK, that's presently unexplored territory!

EDIT: here's a [link to the draft](http://www.mpi-sws.org/~neelk/simple-frp.pdf). 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.

> **Comments:**
> **username_2**: I'd love to get a copy of that when you've finished it.  
> **username_0**: It seems that this loses an important characteristic of futures: once a value is obtained, it can't change. I'd try to express it by taking $A \to \Box A$ as an axiom, but this is not what we want if $\Box$ means a stream... And I'd also like a copy of the paper when it's done :)  
> **username_3**: I recently read that the Scala type `Try[T]` and `Future[T]` are dual, but I have not quite understood what this means / in what sense.  

---

