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:

Futures, presently

The current Future type is just a time and a value, wrapped in a a newtype:

newtype FutureG t a = Future (Time t, a)
  deriving (Functor, Applicative, Monad)

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:

sToF :: Ord t => S.FutureG t a -> F.FutureG t a

fToS :: Ord t => F.FutureG t a -> S.FutureG t a

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:

dToF :: Ord     t => C.FutureG t a -> F.FutureG t a

fToD :: Bounded t => F.FutureG t a -> C.FutureG t a

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.

11 Comments

  1. 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. :-)

  2. 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:

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

    The relative version has only a small change:

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

    where the pad function prepends a segment of ⊥ to a behavior (or any Segment type). (For lists, pad n == (repeat n undefined ++).)

    Equivalently,

    (b `until` Future (t',b')) `at` t
      | t <= t'   = b  `at` t
      | otherwise = b' `at` (t - t')

    Using the ideas in Sequences, streams, and segments and in Sequences, segments, and signals, we get a much more elegant definition:

    b `until` Future (t',b') = take t' b `mappend` b'

    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:

    (b `until` u) `at` t = b'' `at` t
     where
       b'' = case tryFuture u t of
               Nothing              -> b
               Just (Future (_,b')) -> b'

    For relative time,

    (b `until` u) `at` t = b'' `at` t
     where
       b'' = case tryFuture u t of
               Nothing               -> b
               Just (Future (t',b')) -> pad t' b'

    I don’t know how to extend the more elegant take/mappend version to use tryFuture.

  3. Luke Palmer:

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

    order :: Future a -> Future a -> Future (a, Future a)
    order (t,a) (t',b)
     | t <= t'   = (t,  (a, (t', b)))
     | otherwise = (t', (b, (t,  a)))
    

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

  4. Ryan Ingram:

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

  5. conal:

    Luke,

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

    order :: Future a -> Future a -> Future (a, Future a)
    order (t,a) (t',b)
     | t <= t'   = (t,  (a, (t'-t, b)))
     | otherwise = (t', (b, (t-t', a)))

    Then use this order function to define mappend on events (temporal interleaving).

  6. conal:

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

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

  8. Conal Elliott » Blog Archive » Exact numeric integration:

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

  9. 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) benign when the new value is semantically equal to the old value. A benign assignment is beneficial when 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.

  10. Mike Sperber:

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

    fToS f = p (unFuture f maxBound)
      where
       p Nothing -> (maxBound, undefined)
       p (Some sf) -> sf
    

    ?

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

  11. 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 than knowledge about 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.

Leave a comment