Functional concurrency with unambiguous choice

The Reactive library implements functional reactive programming (FRP) in a data-driven and yet purely functional way, on top of a new primitive I call “unambiguous choice”, or unamb. This primitive has simple functional semantics and a concurrent implementation. The point is to allow one to try out two different ways to answer the same question, when it’s not known in advance which one will succeed first, if at all.

This post describes and demonstrates unamb and its implementation.

What’s unamb?

The value of a `unamb` b is the more defined of the values a and b. The operation is subject to a semantic precondition, which is that a and b must be equal unless one or both is bottom. It’s this precondition that distinguishes unamb from the ambiguous (nondeterministic) choice operator amb.

This precondition also distinguishes unamb from least upper (information) bound (“lub”). The two operators agree where both are defined, but lub is much more widely defined than unamb is. For instance, consider the pairs (1,⊥) and (⊥,2). The first pair has information only about its first element, while the second pair has information only about its second element. Their lub is (1,2). The triples (1,⊥,3) and (⊥,2,3) are also consistent and have a lub, namely (1,2,3).

Each of these two examples, however, violates unamb‘s precondition, because in each case the values are unequal and not ⊥.

In the examples below, I’ll use “⊥” in place of “undefined“, for brevity.

Parallel or

In spite of its limitation, unamb can do some pretty fun stuff. For instance, it’s easy to implement the famous “parallel or” operator, which yields true if either argument is true, even if one argument is ⊥.

por :: Bool -> Bool -> Bool
a `por` b = (a || b) `unamb` (b || a)

This use of unamb satisfies the precondition, because (||) is “nearly commutative”, i.e., commutative except when one ordering yields ⊥.

This game is useful with any nearly commutative operation that doesn’t always require evaluating both arguments. The general pattern:

parCommute :: (a -> a -> b) -> (a -> a -> b)
parCommute op x y = (x `op` y) `unamb` (y `op` x)

which can be specialized to parallel or and parallel and:

por :: Bool -> Bool -> Bool
por = parCommute (||)
pand :: Bool -> Bool -> Bool
pand = parCommute (&&)

Let’s see if por does the job. First, here’s sequential or:

*Data.Unamb> True || ⊥
*Data.Unamb>|| True
*** Exception: Prelude.undefined

Now parallel or:

*Data.Unamb> True `por` ⊥
*Data.Unamb> ⊥ `por` True

Short-circuiting multiplication

Another example is multiplication optimized for either argument being zero where the other might be expensive. Just for fun, we’ll optimize for an argument of one as well.

ptimes :: (Num a) => a -> a -> a
ptimes = parCommute times
   0 `times` _ = 0
   1 `times` b = b
   a `times` b = a*b

There’s an important caveat: the type a must be flat. Otherwise, the precondition of unamb might not hold. While many Num types are flat, non-flat Num types are also useful, e.g., derivative towers and functions (and indeed, any applicative functor).


*Data.Lub> 0 **** Exception: Prelude.undefined
*Data.Lub>* 0
*** Exception: Prelude.undefined
*Data.Lub> ⊥ `ptimes` 0
*Data.Lub> 0 `ptimes` ⊥


Let’s assume we had ambiguous choice

amb :: a -> a -> IO a

which applies to any two values of the same type, including fully defined, unequal values. Ambiguous choice nondeterministically chooses one or the other of the values, at its own whim, and may yield different results for the same pair of inputs.

Note that the result of amb is in IO because of its impure semantics. The resulting IO action might produce either argument, but it will only produce bottom if both arguments are bottom.

Given amb, unambiguous choice is easy to implement:

unamb :: a -> a -> a
a `unamb` b = unsafePerformIO (a `amb` b)

The unsafePerformIO is actually safe in this situation because amb is deterministic when the precondition of unamb satisfied.

The implementation of amb simply evaluates both arguments in parallel and returns whichever one finishes (reduces to weak head normal form) first. The racing happens via a function race, which works on actions:

race :: IO a -> IO a -> IO a
amb :: a -> a -> IO a
a `amb` b = evaluate a `race` evaluate b

(The actual definitions of unamb and amb are a bit prettier, for point-free fetishists.)

The race function uses some Concurrent Haskell primitives. For each action, race forks a thread that executes a given action and writes the result into a shared mvar. It then waits for the mvar to get written, and then halts the threads.

a `race` b = do v  <- newEmptyMVar
                ta <- forkPut a v
                tb <- forkPut b v
                x  <- takeMVar  v
                killThread ta
                killThread tb
                return x
forkPut :: IO a -> MVar a -> IO ThreadId
forkPut act v = forkIO (act >>= putMVar v)  -- naive version

This implementation of forkPut is a little too simplisitic. In Haskell, doesn’t simply block forever; it raises an exception. That specific exception must be caught and neutralized.

forkPut act v = forkIO ((act >>= putMVar v) `catch` uhandler)
   uhandler (ErrorCall "Prelude.undefined") = return ()
   uhandler err                             = throw err

Now when act evaluates , the exception is raised, the putMVar is bypassed, and then the exception is silenced. The result is that the mvar does not get written, so the other thread in race must win.

But, oops — what if the other thread also evaluates and skips writing the mvar also? In that case, the main thread of race (which might be spun by another race) will block forever, waiting on an mvar that has no writer. This behavior would actually be just fine, since bottom is the correct answer. However, the GHC run-time system won’t stand for it, and cleverly raises an BlockedOnDeadMVar exception. For this reason, forkPut must neutralize a second exception via a second handler:

forkPut act v = forkIO ((act >>= putMVar v)
                        `catch` uhandler `catch` bhandler)
   uhandler (ErrorCall "Prelude.undefined") = return ()
   uhandler err                             = throw err
   bhandler BlockedOnDeadMVar               = return ()

What’s next?

You can learn more about unamb on the unamb wiki page (where you’ll find links to the code) and in the paper Simply efficient functional reactivity.

My next post will show how to relax the stringent precondition on unamb into something more like the full least-upper-bound operation. This generalization supports richly structured (non-flat) types.


  1. Conal Elliott » Blog Archive » Merging partial values:

    [...] About « Functional concurrency with unambiguous choice [...]

  2. Conal Elliott » Blog Archive » Smarter termination for thread racing:

    [...] shower this morning that there’s a serious flaw in my unamb implementation as described in Functional concurrency with unambiguous choice. Here’s the code for racing two [...]

  3. Conal Elliott » Blog Archive » Another angle on functional future values:

    [...] 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 Simply efficient functional reactivity and the post Functional concurrency with unambiguous choice. [...]

  4. Conal Elliott » Blog Archive » Lazier function definitions by merging partial values:

    [...] like zip above, where we want unbiased laziness. (See posts on unambiguous choice and especially Functional concurrency with unambiguous choice.) The unamb operator returns the more defined of its two arguments, which are required to be equal [...]

  5. Peter Berry:

    In Haskell, ⊥ doesn’t simply block forever; it raises an exception.

    Bit of a nitpick here: ⊥ is not a Haskell expression, but the denotational semantics of undefined. The operational semantics of undefined (at least in GHC) is indeed to raise an exception, but other expressions denoting ⊥ may have other operational semantics (including blocking forever, since the halting problem is undecidable).

    Speaking of which, you probably want to catch NonTermination as well :)

  6. conal:

    Thanks for the comment, Peter. Please note from my post:

    In the examples below, I’ll use “⊥” in place of “undefined“, for brevity.

    I’m making the same conventional pun as with “3″ when describing an expression and when describing a denotation. Haskell was originally designed when we were stuck with ASCII, but we aren’t any longer.

    I do appreciate care in distinguishing syntax from semantics. And I can see how using notation like “3″ or “⊥” in both situations might confuse.

    Also, I’ve taken care to treat all operational variations of ⊥ in a denotationally consistent way, including non-termination. If you think there’s a denotational inconsistency, could you please say what?

Leave a comment