haskell - 操作真的与自由单子(monad)同构吗？

Question

证明

在 this博文中，Tekmo 指出我们可以证明 ExitSuccess退出是因为(我想)它就像 Const该构造函数的仿函数(它不携带 x 所以 fmap 的行为类似于 const )。

使用操作包，Tekmo 的 TeletypeF可能翻译成这样:

data TeletypeI a where
    PutStrLn :: String -> TeletypeI ()
    GetLine :: TeletypeI String
    ExitSuccess :: TeletypeI ()

我读过操作与自由单子(monad)同构，但我们可以在这里证明 ExitSuccess退出？在我看来，它的问题与 exitSuccess :: IO () 完全相同。确实如此，特别是如果我们要为它编写一个解释器，我们需要像它没有退出一样编写它:

eval (ExitSuccess :>>= _) = exitSuccess

与不涉及任何模式通配符的免费 monad 版本相比:

run (Free ExitSuccess) = exitSuccess

懒惰

在 Operational Monad Tutorial apfelmus 提到了一个缺点:

The state monad represented as s -> (a,s) can cope with some infinite programs like

evalState (sequence . repeat . state $ \s -> (s,s+1)) 0

whereas the list of instructions approach has no hope of ever handling that, since only the very last Return instruction can return values.

对于免费的单子(monad)也是如此吗？

Answer 1

(请允许我通过大胆地结合以前的答案来获得大奖。;-))

关键的观察是这样的:证明到底是什么？ Free TeletypeF 的公式允许我们证明以下内容:

Every interpreter for programs of type Free TeletypeF a must exit when it encounters the ExitSuccess instruction. In other words, we automatically get the algebraic law

 interpret (exitSuccess >>= k) = interpret exitSuccess

因此， Free monad 实际上允许您将某些代数定律烘焙到类型中。

相比之下，操作方法不限制 ExitSuccess 的语义。 ，没有与每个解释器相关的相关代数定律。可以编写在遇到该指令时退出的解释器，但也可以编写不退出的解释器。

当然，您可以通过检查证明任何特定的解释器都满足法律，例如因为它使用通配符模式匹配。 Sjoerd Visscher 观察到，您还可以通过更改 ExitSuccess 的返回类型在类型系统中强制执行此操作。至 Void .然而，这不适用于其他可以融入自由单子(monad)的定律，例如 mplus 的分配定律。操作说明。

因此，在一个令人困惑的事件转折中，如果您将“自由”解释为“最少的代数定律”，那么操作方法比自由单子(monad)更自由。

这也意味着这些数据类型不是同构的。然而，它们是等价的:每个解释器都用 Free 编写。可以转换为用 Program 编写的解释器反之亦然。

就个人而言，我喜欢将我所有的法则都放入解释器中，因为有很多法则无法融入自由单子(monad)，我喜欢将它们全部放在一个地方。