## Another angle on functional future values

An earlier post introduced functional *future values*, which are values that cannot be known until the future, but can be manipulated in the present.
That post presented a simple denotational semantics of future values as time/value pairs.
With a little care in the definition of `Time`

(using the `Max`

monoid), the instances of `Functor`

, `Applicative`

, `Monad`

are all derived automatically.

A follow-up post gave an implementation of *Future values via multi threading*.
Unfortunately, that implementation did not necessarily satisfy the semantics, because it allowed the nondeterminism of thread scheduling to leak through.
Although the implementation is usually correct, I wasn’t satisfied.

After a while, I hit upon an idea that really tickled me.
My original simple semantics could indeed serve as a correct and workable implementation if I used a subtler form of time that could reveal partial information.
Implementing this subtler form of time turned out to be quite tricky, and was my original motivation for the `unamb`

operator described in the paper *Push-pull functional reactive programming* and the post *Functional concurrency with unambiguous choice*.

It took me several days of doodling, pacing outside, and talking to myself before the idea for `unamb`

broke through.
Like many of my favorite ideas, it’s simple and obvious in retrospect: to remove the ambiguity of nondeterministic choice (as in the `amb`

operator), restrict its use to values that are equal when non-bottom.
Whenever we have two different methods of answering the same question (or possibly failing), we can use `unamb`

to try them both.
Failures (errors or non-termination) are no problem in this context.
A more powerful variation on `unamb`

is the least upper bound operator `lub`

, as described in *Merging partial values*.

I’ve been having trouble with the `unamb`

implementation.
When two (compatible) computations race, the loser gets killed so as to free up cycles that are no longer needed.
My first few implementations, however, did not recursively terminate *other* threads spawned in service of abandoned computations (from nested use of `unamb`

).
I raised this problem in *Smarter termination for thread racing*, which suggested some better definitions.
In the course of several helpful reader comments, some problems with my definitions were addressed, particularly in regard to blocking and unblocking exceptions.
None of these definitions so far has done the trick reliably, and now it looks like there is a bug in the GHC run-time system.
I hope the bug (if there is one) will be fixed soon, because I’m seeing more & more how `unamb`

and `lub`

can make functional programming even more modular (just as laziness does, as explained by John Hughes in *Why Functional Programming Matters*).

I started playing with future values and unambiguous choice as a way to implement Reactive, a library for functional reactive programming (FRP).
(See *Reactive values from the future* and *Push-pull functional reactive programming*.)
Over the last few days, I’ve given some thought to ways to implement future values without unambiguous choice.
This post describes one such alternative.

**Edits**:

- 2010-08-25: Replaced references to
*Simply efficient functional reactivity*with*Push-pull functional reactive programming*. The latter paper supercedes the former. - 2010-08-25: Fixed the
`unFuture`

field of FutureG to be`TryFuture`

.

### Futures, presently

The current `Future`

type is just a time and a value, wrapped in a a `newtype`

:

Where the `Time`

type is defined via the `Max`

monoid.
The derived instances have exactly the intended meaning for futures, as explained in the post *Future values* and the paper *Push-pull functional reactive programming*.
The “G” in the name `FutureG`

refers to generalized over time types.

Note that `Future`

is parameterized over both time and value.
Originally, I intended this definition as a denotational semantics of future values, but I realized that it could be a workable implementation with a lazy enough `t`

.
In particular, the times have to reveal lower bounds and allow comparisons before they’re fully known.

Warren Burton explored an applicable notion in the 1980s, which he called “improving values”, having a concurrent implementation but deterministic functional semantics.
(See the paper *Encapsulating nondeterminacy in an abstract data type with deterministic semantics* or the paper *Indeterminate behavior with determinate semantics in parallel programs*.
I haven’t found a freely-available online copy of either.)
I adapted Warren’s idea and gave it an implementation via `unamb`

.

Another operation finds the earlier of two futures.
This operation has an identity and is associative, so I wrapped it up as a `Monoid`

instance:

instance (Ord t, Bounded t) => Monoid (FutureG t a) where mempty = Future (maxBound, undefined) Future (s,a) `mappend` Future (t,b) = Future (s `min` t, if s <= t then a else b)

This `mappend`

definition could be written more simply:

u@(Future (t,_)) `mappend` u'@(Future (t',_)) = if t <= t' then u else u'

However, the less simple version has more potential for laziness. The time type might allow yielding partial information about a minimum before both of its arguments are fully known, which is the case with improving values.

### Futures as functions

The Reactive library uses futures to define and implement reactivity, i.e., behaviors specified piecewise.
Simplifying away the notion of *events* for now,

until :: BehaviorG t a -> FutureG t (BehaviorG t a) -> BehaviorG t a

The semantics (but not implementation) of `BehaviorG`

is given by

at :: BehaviorG t a -> (t -> a)

The semantics of `until`

:

(b `until` Future (t',b')) `at` t = b'' `at` t where b'' = if t <= t' then b else b'

FRP (multi-occurrence) events are then built on top of future values, and reactivity on top of `until`

.

The semantics of `until`

shows what information we need from futures: given a time `t`

, we need to know whether `t`

is later than the future’s time and, *if so*, what the future’s value is.
For other purposes, we’ll also want to know the future’s time, but again, only once we’re past that time.
We might, therefore, represent futures as a function that gives exactly this information.
I’ll call this function representation “function futures” and use the prefix “S” to distinguish the original “simple” futures from these function futures.

type TryFuture t a = Time t -> Maybe (S.FutureG t a) tryFuture :: F.FutureG t a -> TryFuture t a

Given a probe time, `tryFuture`

gives `Nothing`

if the time is before or at the future’s time, or `Just u`

otherwise, where `u`

is the simple future.

We could represent `F.FutureG`

simply as `TryFuture`

:

type F.FutureG = TryFuture -- first try

But then we’d be stuck with the `Functor`

and `Applicative`

instances for functions instead of futures.
Adding a `newtype`

fixes that problem:

newtype FutureG t a = Future { unFuture :: TryFuture t a } -- second try

With this representation we can easily construct and try out function futures:

future :: TryFuture t a -> FutureG t a future = Future tryFuture :: FutureG t a -> TryFuture t a tryFuture = unFuture

I like to define helpers for working inside representations:

inFuture :: (TryFuture t a -> TryFuture t' a') -> (FutureG t a -> FutureG t' a') inFuture2 :: (TryFuture t a -> TryFuture t' a' -> TryFuture t'' a'') -> (FutureG t a -> FutureG t' a' -> FutureG t'' a'')

The definitions of these helpers are very simple with the ideas from *Prettier functions for wrapping and wrapping* and a lovely notation from Matt Hellige’s *Pointless fun*.

inFuture = unFuture ~> Future inFuture2 = unFuture ~> inFuture (~>) :: (a' -> a) -> (b -> b') -> ((a -> b) -> (a' -> b')) g ~> h = result h . argument g

These helpers make for some easy definitions in the style of *Semantic editor combinators*:

instance Functor (FutureG t) where fmap = inFuture.fmap.fmap.fmap instance (Bounded t, Ord t) => Applicative (FutureG t) where pure = Future . pure.pure.pure (<*>) = (inFuture2.liftA2.liftA2) (<*>)

#### Type composition

These `Functor`

and `Applicative`

instances (for `FutureG t`

) may look mysterious, but they have a common and inevitable form.
Every type whose representation is the (semantic and representational) composition of three functors has this style of `Functor`

instance, and similarly for `Applicative`

.

Instead of repeating this common pattern, let’s make the type composition explicit, using `Control.Compose`

from the TypeCompose library:

type FutureG t = (->) (Time t) :. Maybe :. S.FutureG t -- actual definition

Now we can throw out `inFuture`

, `inFuture2`

, `(~>)`

, and the `Functor`

and `Applicative`

instances.
These instances follow from the general instances for type composition.

#### Monoid

The `Monoid`

instance could also come automatically from type composition:

instance Monoid (g (f a)) => Monoid ((g :. f) a) where { mempty = O mempty; mappend = inO2 mappend }

The `O`

here is just the `newtype`

constructor for `(:.)`

, and the `inO2`

function is similar to `inFuture2`

above.

However, there is another often-useful `Monoid`

instance:

-- standard Monoid instance for Applicative applied to Monoid instance (Applicative (g :. f), Monoid a) => Monoid ((g :. f) a) where { mempty = pure mempty; mappend = liftA2 mappend }

Because these two instances “overlap” are are both useful, neither one is declared in the general case. Instead, specialized instances are declared where needed, e.g.,

instance (Ord t, Bounded t) => Monoid (FutureG t a) where mempty = ( O . O ) mempty -- or future mempty mappend = (inO2.inO2) mappend

How does the `Monoid`

instance work? Start with `mempty`

. Expanding:

mempty == {- definition -} O (O mempty) == {- mempty on functions -} O (O (const mempty)) == {- mempty on Maybe -} O (O (const Nothing))

So, given any probe time, the empty (never-occurring) future says that it does not occur before the probe time.

Next, `mappend`

:

O (O f) `mappend` O (O f') == {- mappend on FutureG -} O (O (f `mappend` f')) == {- mappend on functions -} O (O (\ t -> f t `mappend` f' t)) == {- mappend on Maybe -} O (O (\ t -> f t `mappendMb` f' t)) where Nothing `mappendMb` mb' = mb' mb `mappendMb` Nothing = mb Just u `mappendMb` Just u' = Just (u `mappend` u')

The `mappend`

in this last line is on simple futures, as defined above, examining the (now known) times and choosing the earlier future.
Previously, I took special care in that `mappend`

definition to enable `min`

to produce information before knowing whether `t <= t'`

.
However, with this new approach to futures, I expect to use simple (flat) times, so it could instead be

u@(Future (s,_)) `mappend` u'@(Future (s',_)) = if s <= s' then u else u'

or

u `mappend` u' = if futTime u <= futTime u' then u else u' futTime (Future (t,_)) = t

or just

`mappend = minBy futTime`

How does `mappend`

work on function futures?
Given a test time `t`

, if both future times are at least `t`

, then the combined future’s time is at least `t`

(yielding `Nothing`

).
If either future is before `t`

and the other isn’t, then the combined future is the same as the one before `t`

.
If both futures are before `t`

, then the combined future is the earlier one.
Exactly the desired semantics!

#### Relating function futures and simple futures

The function-based representation of futures relates closely to the simple representation. Let’s make this relationship explcit by defining mappings between them:

The first one is easy:

sToF u@(S.Future (t, _)) = future (\ t' -> if t' <= t then Nothing else Just u)

The reverse mapping, `fToS`

, is trickier and is only defined on the image (codomain) of `sToF`

.
I think it can be defined mathematically but not computationally.
There are two cases: either the function always returns `Nothing`

, or there is at least one `t`

for which it returns a `Just`

.
If the former, then the simple future is `mempty`

, which is `S.Future (maxBound, undefined)`

.
If the latter, then there is only one such `Just`

, and the simple future is the one in that `Just`

.
Together, `(sToF, fToS)`

form a projection-embedding pair.

We won’t really have to implement or invoke these functions.
Instead, they serve to further specify the type `F.FutureG`

and the correctness of operations on it.
The representation of `F.FutureG`

as given allows many values that do not correspond to futures.
To eliminate these representations, require an invariant that a function future must be the result of applying `sToF`

to some simple future.

We’ll require that each operation preserves this invariant.
However, let’s prove something stronger, namely that operations on on `F.FutureG`

correspond precisely to the same operations on `S.FutureG`

, via `sToF`

.
In other words, `sToF`

preserves the shape of the operations on futures.
For type classes, these correspondences are the type class morphisms.
For instance, `sToF`

is a `Monoid`

morphism:

sToF mempty == mempty sToF (u `mappend` u') == sToF u `mappend` sToF u'

### Caching futures

This function representation eliminates the need for tricky times (using improving values and `unamb`

), but it loses the caching benefit that lazy functional programming affords to non-function representations.
Now let’s reclaim that benefit.
The trick is to exploit the restriction that every function future must be
(semantically) the image of a simple future under `sToF`

.

Examining the definition of `sToF`

, we can deduce the following monotonicity properties of (legitimate) function futures:

- If the probe function yields
`Nothing`

for some`t'`

, then it yields`Nothing`

for earlier times. - If the probe function yields
`Just u`

for some`t'`

, then it yields`Just u`

for all later times.

We can exploit these monotonicity properties by caching information as we learn it. Caching of this sort is what distinguishes call-by-need from call-by-name and allows lazy evaluation to work efficiently for data representations.

Specifically, let’s save a best-known lower bound for the future time and the simple future when known.
Since the lower bound may get modified a few times, I’ll use a `SampleVar`

(thread-safe rewritable variable).
The simple future will be discovered only once, so I’ll use an `IVar`

.
I’ll keep the function-future for probing when the cached information is not sufficient to answer a query.

Prefix this caching version with a “C”, to distinguish it from function futures (“F”) and the simple futures (“S”):

data C.FutureG t a = Future (SampleVar t) (IVar (S.FutureG t a)) (F.FutureG t a)

Either the simple future or the function future will be useful, so we could replace the second two fields with a single one:

data C.FutureG t a = Future (SampleVar t) (MVar (Either (F.FutureG t a) (FF.FutureG t a)))

We’ll have to be careful about multiple independent discoveries of the same simple future, which would correspond to multiple writes `IVar`

with the same value.
(I imagine there are related mechanics in the GHC RTS for two threads evaluating the same thunk that would be helpful to understand.)
I guess I could use a `SampleVar`

and just not worry about multiple writes, since they’d be equivalent.
For now, use the `IVar`

version.

The caching representation relates to the function representation by means of two functions:

The implementation

dToF (C.Future tv uv uf) = F.Future $ \ t' -> unsafePerformIO $ do mb <- tryReadIVar uv case mb of j@(Just (S.Future (Max t,_))) -> return (if t' <= t then Nothing else j) Nothing -> do tlo <- readSampleVar tv if t' <= tlo then return Nothing else do let mb' = F.unFuture uf t' writeIVarMaybe uv mb' return mb' -- Perhaps write to an IVar writeIVarMaybe :: IVar a -> Maybe a -> IO () writeIVarMaybe v = maybe (return ()) (writeIVar v) fToD uf = unsafePerformIO $ do tv <- newSampleVar t0 uv <- newIVar writeIVarMaybe uv (F.unFuture uf t0) return (Future tv uv uf) where t0 = minBound

It’ll be handy to delegate operations to `F.Future`

:

inF :: (Ord t, Bounded t') => (F.FutureG t a -> F.FutureG t' a') -> ( FutureG t a -> FutureG t' a') inF = dToF ~> fToD inF2 :: (Ord t, Bounded t', Ord t', Bounded t'') => (F.FutureG t a -> F.FutureG t' a' -> F.FutureG t'' a'') -> ( FutureG t a -> FutureG t' a' -> FutureG t'' a'') inF2 = dToF ~> inF

Then

instance (Ord t, Bounded t) => Monoid (FutureG t a) where mempty = fToD mempty mappend = inF2 mappend instance (Ord t, Bounded t) => Functor (FutureG t) where fmap = inF . fmap instance (Ord t, Bounded t) => Applicative (FutureG t) where pure = fToD . pure (<*>) = inF2 (<*>)

### Wrap-up

Well, that’s the idea. I’ve gotten as far as type-checking the code in this post, but I haven’t yet tried running it.

What interests me most above is the use of `unsafePerformIO`

here while preserving referential transparency, thanks to the invariant on `F.FutureG`

(and the consequent monotonicity property).
The heart of lazy evaluation of *pure* functional programs is just such an update, replacing a thunk with its weak head normal form (whnf).
What general principles can we construct that allow us to use efficient, destructive updating and still have referential transparency?
The important thing above seems to be the careful definition of an abstract interface such that the effect of state updates is semantically invisible through the interface.

## Creighton Hogg:

Thanks for writing these ideas up. A quick question, though: it seems like this definition of Futures really only makes sense for absolute time?

Also, I understand why it’s okay to use unsafePerformIO here but it still makes me a little squeamish. I don’t trust myself with that abstraction-breaking hammer yet.

5 January 2009, 7:24 am## conal:

Hi Creighton. Thanks for the question.

I think what makes these futures be absolute time is the use of the

`Max`

monoid. Switching to the`Sum`

monoid gives relative time. Moreover, the definition of`until`

needs some tweaking.Absolute version:

The relative version has only a small change:

where the

`pad`

function prepends a segment of ⊥ to a behavior (or any`Segment`

type). (For lists,`pad n == (repeat n undefined ++)`

.)Equivalently,

Using the ideas in

Sequences, streams, and segmentsand inSequences, segments, and signals, we get a much more elegant definition:This formulation is what inspired those two blog posts and my renewed interest in relative time FRP.

With function futures or caching futures,

`until`

would look like the following for absolute time:For relative time,

I don’t know how to extend the more elegant

5 January 2009, 10:47 am`take`

/`mappend`

version to use`tryFuture`

.## Luke Palmer:

I still claim that you can and should encapsulate your Future representation by the use of the order combinator:

So that the rest of the reactive code can be independent of your representation.

Oh, and this looks like a nice lead, by the way.

5 January 2009, 12:28 pm## Ryan Ingram:

Is “SampleVar” documented anywhere? It’s an abstraction I’m unaware of at this moment.

5 January 2009, 1:50 pm## conal:

Luke,

Thanks for the great suggestion! It also feeds very nicely into relative time:

Then use this

5 January 2009, 1:59 pm`order`

function to define`mappend`

on events (temporal interleaving).## conal:

Ryan — Yes. See the link where I first mention SampleVar above.

5 January 2009, 6:05 pm## Patai Gergely:

I’ve been looking at this post for a while, but I still can’t see why you need to add all this complexity. Couldn’t you achieve the same thing by simply using an IORef that starts out as Nothing and is assigned exactly once, when the event actually fires?

What exactly does your code do when you are trying to sample the far future? I don’t understand where the magic future function comes from that can handle this case, but I assume this is what the (imperative?) framework should provide. And again, if we never want to sample with a future time, how is this different from an IORef after all and why is it better?

Gergely

19 January 2009, 2:37 am## Conal Elliott » Blog Archive » Exact numeric integration:

[...] This benign-update idea is also explored in Another angle on functional future values. [...]

28 December 2009, 10:26 am## conal:

Hi Gergely:

Please note the second paragraph in this post. What I’m going for here is a simple & precise semantics and a faithful implementation. If I understand your suggestion, it would be a simple implementation but I doubt it would be faithful to a simple & precise semantics. Maybe it could be faithful under certain assumptions about single- vs multi-threading, what it means for events to fire (in the imperative substrate), and how the resulting assignments interact with the mechanics of functional evaluation in the Haskell run-time system. I imagine following this path would require some very complicated reasoning and would yield fairly restrictive results. If anyone does try to apply rigorous reasoning to your suggestion, I’d be very interested in reading about the results.

If you ignore the “caching futures” aspect of this post, I hope you can see the answer to your question of sampling into the far future.

In the caching section, I’m reaching for general principles for extending the laziness machinery that we already know & love, while keeping its semantic purity. What justifies claiming purely functional semantics in the presence of these side-effects? In other words, what makes some assignments (semantically) benign and others malignant?

In brief, assignment is (semantically)

benignwhen the new value is semantically equal to the old value. A benign assignment isbeneficialwhen it improves some sort of efficiency. As an example, to implement laziness, the run-time system performs thunk overwriting. The old thunk and the new value (whnf) are semantically equal. The benefit is improved speed of access, perhaps at the cost of space.I would like to explore the space of beneficial, benign assignments much more thoroughly than this one special case of thunk overwriting.

24 August 2010, 7:15 pm## Mike Sperber:

I’m not sure I understand the comment about fToS not lending itself to implementation. Can’t you say (rusty Haskell ahead):

?

Sure, you might have to wait, but that’s true in general of F.FutureG, no?

12 July 2011, 1:33 am## Mike Sperber:

Getting back to my previous comment: I think I understand what the issue is now, and it reveals a deeper problem with this approach to future value:

You start out by saying that all function futures should be created from simple futures, but of course caching futures violate that principle – at least if they themselves are not created from simple futures. And, at some point, you want to hook up actual external-world actions to get some of that reactivity the “R” in FRP is about, and caching futures are an entry obvious entry point.

Here’s the problem: Caching futures themselves are well-behaved, but caching futures combined with mappend are not: Consider two caching futures

`f1`

and`f2`

, and only`f1`

gets triggered at time`t0`

. Mappend them to get future`f`

. If you ask the (try-future version of) f at time`t' > t0`

, you get`Some`

answer. If you ask at`MaxBound`

(which is greater than`t'`

), you get no answer, because the system waits for`f2`

. So monotonicity is violated. That, of course, is also the issue with my version of`fToS`

.The deeper problem, I think, is the fact that the event occurrences the system talks about really refer to the programmatic event (i.e. the

`SampleVar`

being filled), rather thanknowledgeabout an external event, which only becomes available after it has actually happened. (How do you mappend two futures knowing that they’ll become known only after the timestamps that will be attached to them?)All solutions I’ve come up with for this require going back to some notion of partial time. It can be pushed into a smaller corner than before, but it’s still there.

19 October 2011, 11:22 pm