## 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 || ⊥
True

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

Now parallel or:

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

*Data.Unamb> ⊥ `por` True
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
where
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).

Testing:

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

### Implementation

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
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)
where
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)
where
uhandler (ErrorCall "Prelude.undefined") = return ()
uhandler err                             = throw err
``````

### 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?