在功能反应式编程中,如何在应用程序的两个部分之间共享状态？

Question

我有一些应用程序架构,其中用户输入流到某些自动机,它在事件流的上下文中运行,并将用户引导到应用程序的不同部分.应用程序的每个部分都可以根据用户输入执行某些操作.但是,应用程序的两个部分是共享某个状态,并且在概念上是读取和写入同一个状态.需要注意的是,两个"线程"没有同时运行,其中一个"暂停"而另一个"产生"输出.描述这种状态共享计算的规范方法是什么,而不需要求助于某些全局变量？两个"线程"是否有意义保持本地状态通过某种形式的消息传递同步,即使它们不是以任何方式并发？

没有代码示例,因为问题更具概念性,但欢迎使用Haskell(使用任何FRP框架)或其他语言的示例答案.

Answer 1

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

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

B)单线程规范用于StateT共享公共状态

整体架构的灵感来自模型 - 视图 - 控制器.你有:

• 控制器,是有效的输入
• 视图,这是有效的输出
• 一个模型,这是一个纯粹的流转换

该模型只能与一个控制器和一个视图交互.但是,控制器和视图都是幺半群,因此您可以将多个控制器组合到一个控制器中,将多个视图组合到一个视图中.从图中可以看出,它看起来像这样:

 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库的目的是为控制台提供一个并发接口,使您可以在同时打印到控制台的同时读取用户的输入,但不会打印输出,从而破坏用户的输入.它的Github存储库在这里:

链接到Github存储库

我对这个库的原始实现具有普遍的并发性和消息传递,但是受到了几个我无法解决的并发错误的困扰.然后当我提出mvc(我的类似FRP的框架的代号,"模型 - 视图 - 控制器"的缩写)时,我认为这rcpl将是一个很好的测试用例,看看是否mvc准备好黄金时段.

我把它的整个逻辑都rcpl变成了一个纯粹的管道.这就是您将在此模块中找到的内容,并且总逻辑完全包含在rcplCore管道中.

这很简洁,因为现在实现是纯粹的,我可以快速检查它并验证某些属性!例如,我可能想要快速检查的一个属性是按键的每个用户键只有一个终端命令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发现我的财产是假的!此外,由于代码是引用透明的,因此QuickCheck可以将反例缩小到最小再现违规.按下78键之后,终端驱动程序会发出换行符,因为控制台宽度为80个字符,并且提示符占用了两个字符("> "在本例中).这就是我很难验证并发和IO感染整个系统的那种属性.

有一个纯粹的设置是很好的另一个原因:一切都是完全可重复的!如果我存储所有传入事件的日志,那么任何时候出现错误我都可以重放事件并完美地复制我可以添加到测试套件的测试用例.

然而,纯度最重要的好处是能够更容易地非正式地和正式地推理代码.当您从等式中删除Haskell的调度程序时,您可以静态地证明代码,当您必须依赖具有非正式指定语义的并发运行时时,无法证明这些代码.这实际上证明了即使对于非正式推理也非常有用,因为当我转换我的代码使用mvc它时仍然有几个错误,但这些比我第一次迭代中的顽固并发错误更容易调试和删除.

该rcpl示例用于StateT在不同组件之间共享全局状态,因此对您的问题的冗长答案是:您可以使用StateT,但前提是您将系统转换为单线程版本.幸运的是,这是可能的!