我一直在努力解决这个问题。概括地说,您:
A) 将所有并发代码提炼成纯单线程规范
B) 单线程规范使用StateT 共享公共状态
整体架构的灵感来自模型-视图-控制器。你有:
- 控制器,它们是有效的输入
- 视图,即有效输出
- 一个模型,它是一个纯流转换
模型只能与一个控制器和一个视图交互。但是,控制器和视图都是 monoid,因此您可以将多个控制器组合成一个控制器,将多个视图组合成一个视图。从图表上看,它看起来像这样:
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 以跟踪共享状态。在这种情况下,pipes 符合要求。
最后一块拼图是一个复杂的现实世界示例,它采用复杂的并发系统并将其提炼成一个纯单线程等价物。为此,我使用了我即将推出的 rcpl 库(“read-concurrent-print-loop”的缩写)。 rcpl 库的目的是为控制台提供一个并发接口,使您可以在同时打印到控制台的同时读取用户的输入,但打印的输出不会破坏用户的输入。它的 Github 存储库在这里:
Link to Github Repository
我最初的这个库实现具有普遍的并发性和消息传递,但受到几个我无法解决的并发错误的困扰。然后当我想出mvc(我的类似 FRP 的框架的代号,“model-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 发现我的属性是假的!此外,由于代码是引用透明的,QuickCheck 可以将反例缩小到最小再现违规。按下 78 键后,终端驱动程序会发出换行符,因为控制台有 80 个字符宽,并且提示占用了两个字符(在这种情况下为"> ")。如果并发和IO 感染了我的整个系统,我将很难验证这种属性。
拥有一个纯粹的设置是伟大的另一个原因:一切都是完全可重现的!如果我存储了所有传入事件的日志,那么只要有错误,我就可以重播这些事件,并拥有完美再现的测试用例,我可以将其添加到我的测试套件中。
然而,纯度最重要的好处是能够更轻松地以非正式和正式方式推理代码。当您从等式中删除 Haskell 的调度程序时,您可以静态地证明您的代码在必须依赖具有非正式指定语义的并发运行时时无法证明的事情。这实际上被证明是非常有用的,即使是非正式的推理,因为当我将代码转换为使用 mvc 时,它仍然有几个错误,但这些比我第一次迭代中顽固的并发错误更容易调试和删除。
rcpl 示例使用StateT 在不同组件之间共享全局状态,因此对您的问题的冗长回答是:您可以使用StateT,但前提是您将系统转换为单线程版本。幸运的是,这是可能的!