In functional reactive programming, how do you share state between two parts of the application?

Question

I have some application architecture where user inputs flow to some automata, which runs in the context of the event stream and directs the user to different part of the application. Each part of the application may run some action based on user inputs. However, two parts of the application is sharing some state and are, conceptually, reading and writing to the same state. The caveat is that the two "threads" are not running at the same time, one of them is "paused" while the other one "yields" outputs. What is the canonical way to describe this state sharing computation, without resorting to some global variable? Does it make sense for the two "threads" to keep local states that sync by some form of message passing, even though they are not concurrent by any means?

There is no code sample since the question is more conceptual, but answers with sample in Haskell (using any FRP framework) or some other language is welcomed.

Answer 1

I've been working on a solution to this problem. The high-level summary is that you:

A) Distill all your concurrent code into a pure and single-threaded specification

B) The single-threaded specification uses StateT to share common state

The overall architecture is inspired by model-view-controller. You have:

• Controllers, which are effectful inputs
• Views, which are effectful outputs
• A model, which is a pure stream transformation

The model can only interact with one controller and one view. However, both controllers and views are monoids, so you can combine multiple controllers into a single controller and multiple views into a single view. Diagrammatically, it looks like this:

 controller1 -                                           -> view1
              \                                         /
 controller2 ---> controllerTotal -> model -> viewTotal---> view2
              /                                         \
 controller3 -                                           -> view3

                  \______ ______/   \__ __/   \___ ___/
                         v             v          v
                     Effectful        Pure    Effectful

The model is a pure, single-threaded stream transformer that implements Arrow and ArrowChoice. The reason why is that:

• Arrow is the single-threaded equivalent to parallelism
• ArrowChoice is the single-threaded equivalent to concurrency

In this case, I use push-based pipes, which appear to have a correct Arrow and ArrowChoice instance, although I'm still working on verifying the laws, so this solution is still experimental until I complete their proofs. For those who are curious, the relevant type and instances are:

newtype Edge m r a b = Edge { unEdge :: a -> Pipe a b m r }

instance (Monad m) => Category (Edge m r) where
    id = Edge push
    (Edge p2) . (Edge p1) = Edge (p1 >~> p2)

instance (Monad m) => Arrow (Edge m r) where
    arr f = Edge (push />/ respond . f)
    first (Edge p) = Edge $ \(b, d) ->
        evalStateP d $ (up \>\ unsafeHoist lift . p />/ dn) b
      where
        up () = do
            (b, d) <- request ()
            lift $ put d
            return b
        dn c = do
            d <- lift get
            respond (c, d)

instance (Monad m) => ArrowChoice (Edge m r) where
    left (Edge k) = Edge (bef >=> (up \>\ (k />/ dn)))
      where
          bef x = case x of
              Left b -> return b
              Right d -> do
                  _ <- respond (Right d)
                  x2 <- request ()
                  bef x2
          up () = do
              x <- request ()
              bef x
          dn c = respond (Left c)

The model also needs to be a monad transformer. The reason why is that we want to embed StateT in the base monad to keep track of shared state. In this case, pipes fits the bill.

The last piece of the puzzle is a sophisticated real-world example of taking a complex concurrent system and distilling it into a pure single-threaded equivalent. For this I use my upcoming rcpl library (short for "read-concurrent-print-loop"). The purpose of the rcpl library is to provide a concurrent interface to the console that lets you read input from the user while concurrently printing to the console, but without the printed output clobbering the user's input. The Github repository for it is here:

Link to Github Repository

My original implementation of this library had pervasive concurrency and message passing, but was plagued by several concurrency bugs which I could not solve. Then when I came up with mvc (the code name for my FRP-like framework, short for "model-view-controller"), I figured that rcpl would be an excellent test case to see if mvc was ready for prime-time.

I took the entire logic of the rcpl and turned it into a single, pure pipe. That's what you will find in this module, and the total logic is contained entirely within the rcplCore pipe.

This is neat, because now that the implementation is pure, I can quickcheck it and verify certain properties! For example, one property I might want to quickcheck is that there is exactly one terminal command per user key press of the x key, which I would specify like this:

>>> quickCheck $ \n -> length ((`evalState` initialStatus) $ P.toListM $ each (replicate n (Key 'x')) >-> runEdge (rcplCore t)) == n || n < 0

n is the number of times that I press the x key. Running that test produces the following output:

*** Failed! Falsifiable (after 17 tests and 6 shrinks):
78

QuickCheck discovered that my property was false! Moreover, because the code is referentially transparent, QuickCheck can narrow down the counterexample to the minimal-reproducing violation. After 78 key presses the terminal driver emits a newline because the console is 80 characters wide, and two characters are taken up by the prompt ("> " in this case). That's the kind of property I would have great difficult verifying if concurrency and IO infected my entire system.

Having a pure setup is great for another reason: everything is completely reproducible! If I store a log of all incoming events, then any time there is a bug I can replay the events and have perfectly reproducing test case that I can add to my test suite.

However, really the most important benefit of purity is the ability to more easily reason about code, both informally and formally. When you remove Haskell's scheduler from the equation you can prove things statically about your code that you couldn't prove when you have to depend on a concurrent runtime with an informally specified semantics. This actually proved to be really useful even for informal reasoning, because when I transformed my code to use mvc it still had several bugs, but these were far easier to debug and remove than the stubborn concurrency bugs from my first iteration.

The rcpl example uses StateT to share global state between different components, so the long-winded answer to your question is: You can use StateT, but only if you transform your system to a single-threaded version. Fortunately that's possible!