操作真的与一个免费的monad同构吗？

Question

证明

在这篇博客文章中,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

怠惰

在操作Monad教程中, apfelmus提到了一个缺点:

状态monad表示为s - >(a,s)可以应对一些无限的程序,如

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

而指令列表方法没有希望处理它,因为只有最后一个Return指令才能返回值.

对于免费的monad也是如此吗？

Answer 1

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

关键的观察是:证明究竟是什么？这个表述Free TeletypeF允许我们证明以下内容:

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

 interpret (exitSuccess >>= k) = interpret exitSuccess

因此,Freemonad实际上允许你将某些代数定律烘焙到类型中.

相反,操作方法不限制语义ExitSuccess,没有与每个解释器相关的相关代数法.可以编写在遇到此指令时退出的解释器,但也可以编写不能解释的解释器.

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

因此,在一个令人困惑的事件转变中,如果你将"自由"解释为"最少量的代数定律",那么操作方法比免费monad更自由.

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

就个人而言,我喜欢把我的所有法律都放到翻译中,因为有许多法律无法融入免费的monad中,我喜欢将它们全部放在一个地方.

Answer 2

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

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

参数TeletypeI是操作将/必须提供给程序的其余部分.它是延续的参数的类型k中

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

由于没有类型的值Void,我们可以肯定k永远不会被调用.(一如既往,我们必须忽略undefined这一点.)

等效类型是:

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

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

同样,exitSuccess可以通过给它类型来修复IO Void,或者IO a.

Answer 3

答案是否定的,你无法证明操作人员忽略了程序的其余部分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.