25

证明

在这篇博文中，Tekmo 指出我们可以证明ExitSuccessexits 因为（我认为）它就像Const那个构造函数的函子（它不携带xso的fmap行为const）。

使用操作包，TekmoTeletypeF可能会被翻译成这样：

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

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

eval (ExitSuccess :>>= _) = exitSuccess

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

run (Free ExitSuccess) = exitSuccess

懒惰

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

表示为 s -> (a,s) 的状态单子可以处理一些无限程序，例如

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

而指令列表方法没有希望处理这个问题，因为只有最后一个 Return 指令可以返回值。

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

4

3 回答 3

16

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

关键的观察是这样的：证明到底是什么？公式Free TeletypeF使我们能够证明以下内容：

每个类型程序的解释器在遇到指令Free TeletypeF a时都必须退出。ExitSuccess换句话说，我们自动得到代数定律

 interpret (exitSuccess >>= k) = interpret exitSuccess

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

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

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

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

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

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

于 2013-01-12T16:45:25.280 回答
11

答案是肯定的，但前提是您使用不同的翻译TeletypeF：

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

的参数TeletypeI是操作将/必须提供给程序的其余部分的内容。它是继续的参数的k类型

eval (ExitSuccess :>>= k) = ...

由于没有 type 的值Void，我们可以确定它k永远不会被调用。（与往常一样，我们必须在undefined这里忽略。）

一个等价的类型是：

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

现在我们必须提供一个k匹配任何类型的值，我们也不能这样做。这可以更实用，因为singleton ExitSuccess现在有灵活的类型Program TeletypeI a。

类似地，exitSuccess可以通过给它 typeIO Void或来修复IO a。

于 2013-01-10T19:54:02.387 回答
5

答案是否定的，你不能证明操作者忽略了程序的其余部分exitSuccess。对比看看为什么TeletypeI。TeletypeF我将TeletypeF用 GADT 符号重写以便于比较

data TeletypeF x where                     | data TeletypeI x where
  PutStrLn :: String -> x  -> TeletypeF x  |   PutStrLn :: String -> TeletypeI ()
  GetLine :: (String -> x) -> TeletypeF x  |   GetLine :: TeletypeI String
  ExitSuccess ::              TeletypeF x  |   ExitSuccess :: TeletypeI ()

使用TeletypeF，我们可以立即构建实际程序：

GetLine (\str -> PutStrLn (map toUpper str) ExitSuccess)

TeletypeI没有以与此相同的方式引用“程序的其余部分”的方法TeletypeF。

-- TeletypeF:
GetLine (\str -> "rest of program" goes here)
-- or
PutStrLn someString ("rest of program" goes here)
-- or
ExitSuccess -- there is no "rest of program" slot provided

由于TeletypeI缺少这个“程序的其余部分”信息，当你遇到ExitSuccess.

-- TeletypeI
PutStrLn someString -- no information about "rest of program"
-- or
GetLine -- no information about "rest of program"
-- or
ExitSuccess -- no information about "rest of program"

作为“程序的其余部分”，允许出现的情况完全取决于Program类型，它对所应用的指令集一无所知。它只是允许您将指令绑定在一起，并通过Return.

于 2013-01-10T18:48:40.793 回答