haskell - 在函数式响应式(Reactive)编程中，如何在应用程序的两个部分之间共享状态？

Question

我有一些应用程序体系结构，其中用户输入流到一些自动机，该自动机在事件流的上下文中运行，并将用户定向到应用程序的不同部分。应用程序的每个部分都可以根据用户输入运行某些操作。但是，应用程序的两个部分共享某些状态，从概念上讲，它们是在同一状态下进行读写。需要注意的是，这两个“线程”不是同时运行的，其中一个是“暂停”的，而另一个是“屈服”的输出。在不诉诸某些全局变量的情况下，描述这种状态共享计算的规范方法是什么？两个“线程”保持通过某种形式的消息传递进行同步的本地状态是否有意义，即使它们并非以任何方式并发？

由于该问题更具概念性，因此没有代码示例，但是欢迎使用Haskell(使用任何FRP框架)或其他某种语言给出示例答案。

Answer 1

我一直在努力解决这个问题。高级摘要是您:

A)将所有并发代码提取为纯单线程规范

B)单线程规范使用StateT共享公共(public)状态

整个体系结构受模型 View Controller 的启发。你有:

Controller ，是有效的输入

View ，是有效的输出

一个模型，它是纯流转换

该模型只能与一个 Controller 和一个 View 交互。但是， Controller 和 View 都是monoid，因此您可以将多个 Controller 组合成一个 Controller ，并将多个 View 组合成一个 View 。用图解法表示，它看起来像这样:

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

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

该模型是实现 Arrow和 ArrowChoice的纯单线程流转换器。原因是:

Arrow是等效于并行性

的单线程

ArrowChoice是与并发

等效的单线程

在这种情况下，尽管我仍在努力验证定律，但我使用的是基于推式的 pipes，它似乎具有正确的 Arrow和 ArrowChoice实例，因此在我完成他们的证明之前，该解决方案仍然是试验性的。对于那些好奇的人，相关的类型和实例是:

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)

该模型还需要是monad变压器。原因是我们希望将 StateT嵌入基本monad中以跟踪共享状态。在这种情况下， pipes符合要求。

难题的最后一部分是一个复杂的现实世界示例，该示例采用复杂的并发系统并将其提炼为纯单线程等效项。为此，我使用了我即将发布的 rcpl库(“read-concurrent-print-loop”的缩写)。 rcpl库的目的是为控制台提供并发接口(interface)，使您可以在同时打印到控制台的同时从用户读取输入，而不会导致打印输出阻塞用户的输入。 Github存储库在这里:

Link to Github Repository

我最初对该库的实现具有广泛的并发性和消息传递功能，但是却遇到了一些我无法解决的并发性错误。然后，当我想到 mvc(类FRP框架的代号，“模型- View - Controller ”的缩写)时，我发现 rcpl将是一个很好的测试用例，以了解 mvc是否已准备就绪。

我采用了 rcpl的全部逻辑，并将其变成单个纯管道。这就是在 this module中可以找到的内容，并且整个逻辑完全包含在 rcplCore pipe中。

这很简单，因为现在实现是纯净的，所以我可以对其进行快速检查并验证某些属性!例如，我可能要快速检查的一个属性是，每按一次 x键，每个用户键正好有一个终端命令，我可以这样指定:

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

n是我按 x键的次数。运行该测试将产生以下输出:

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

QuickCheck发现我的属性(property)是假的!而且，由于代码是参照透明的，因此QuickCheck可以将反例缩小到最小限度的违例。按下78键后，终端驱动程序将发出换行符，因为控制台的宽度为80个字符，并且提示符占用了两个字符(在这种情况下为 "> ")。如果并发和 IO感染了我的整个系统，那么我将很难验证这种属性。

进行纯设置非常有用，这是出于另一个原因:一切都是完全可重现的!如果我存储所有传入事件的日志，那么只要有错误，我就可以重播事件并完美地复制测试用例，然后将其添加到测试套件中。

但是，纯净度最重要的好处实际上是能够更轻松地非正式地和正式地进行代码推理。当从等式中删除Haskell的调度程序时，您可以静态地证明有关代码的事情，而当您不得不依赖具有非正式指定语义的并发运行时时，则无法证明。实际上，即使对于非正式推理，这实际上也非常有用，因为当我将代码转换为使用 mvc时，它仍然存在多个错误，但是与第一次迭代中顽固的并发错误相比，它们更容易调试和删除。
rcpl示例使用 StateT在不同组件之间共享全局状态，因此对该问题的长期回答是:您可以使用 StateT，但前提是您将系统转换为单线程版本。幸运的是，这是可能的!