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
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.
The value of
a `unamb` b is the more defined of the values
The operation is subject to a semantic precondition, which is that
b must be equal unless one or both is bottom.
It’s this precondition that distinguishes
unamb from the ambiguous (nondeterministic) choice operator
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
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.
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
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.
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 0 *Data.Lub> 0 `ptimes` ⊥ 0
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.
amb, unambiguous choice is easy to implement:
unamb :: a -> a -> a a `unamb` b = unsafePerformIO (a `amb` b)
unsafePerformIO is actually safe in this situation because
amb is deterministic when the precondition of
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
amb are a bit prettier, for point-free fetishists.)
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.
⊥ 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
⊥, 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
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 bhandler BlockedOnDeadMVar = return ()
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.