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:
Continue reading ‘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...