运作真的是同构于一个免费的monad吗？ [英] Is operational really isomorphic to a free monad?

问题描述

证明

在这篇博客文章中，Tekmo指出我们可以证明退出 ExitSuccess 是因为（我认为）它就像 Const functor for the constructor（它不包含 x ，所以 fmap 的行为就像
$ b

使用操作包，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提到了一个缺点：$ b​​
$ b

以s - >（a，s）表示的状态monad可以应付一些无限
程序如$ /

$ $ p $ evalState（sequence。repeat。state $ \s - >（s，s + 1）） 0


而指令列表并不希望处理$

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

（请允许我通过大胆地结合以前的答案来获得最高奖项。）

; - ））

关键观察结果如下：证明 究竟是什么？根据 Free TeletypeF 的表述，我们可以证明以下几点：

每个对于类型 Free TeletypeF a 的程序， interpreter 在遇到 ExitSuccess 指令时必须退出。换句话说，我们自动得到代数法

  interpret（exitSuccess>> = k ）=解释exitSuccess 
  

因此，免费 monad实际上允许您将某些代数法律烘焙到该类型中。

相比之下，操作方法不会限制 ExitSuccess ，没有涉及每个解释器的相关代数法则。可以编写在遇到此指令时退出的解释器，但也可以编写不解释的解释器。

当然，您可以证明任何特定口译员通过检查满足法律，例如因为它使用通配符模式匹配。 Sjoerd Visscher注意到，你也可以通过将 ExitSuccess 的返回类型更改为 Void 来在类型系统中强制执行此操作。然而，这不适用于可以融入免费单子的其他法律，例如 mplus 指令的分配法律。

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

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

就我个人而言，我喜欢将所有的法律都放到口译员手中，因为有很多法律不能将 monad，我喜欢将它们放在一个地方。

Proofs

In this blog post, Tekmo makes the point that we can prove that ExitSuccess exits because (I presume) it's like the Const functor for that constructor (it doesn't carry the x so fmap behaves like const).

With the operational package, Tekmo's TeletypeF might be translated something like this:

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

I've read that operational is isomorphic to a free monad, but can we prove here that ExitSuccess exits? It seems to me that it suffers from exactly the same problem as exitSuccess :: IO () does, and in particular if we were to write an interpreter for it, we'd need to write it like as if it didn't exit:

eval (ExitSuccess :>>= _) = exitSuccess

Compare to the free monad version which doesn't involve any pattern wildcard:

run (Free ExitSuccess) = exitSuccess

Laziness

In the Operational Monad Tutorial apfelmus mentions a drawback:

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.

Is this true for free monads as well?

解决方案

(Allow me to scoop the grand prize by boldly combining the previous answers. ;-))

The key observation is this: Prove what exactly? The formulation in terms of Free TeletypeF allows us to prove the following:

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

Thus, the Free monad actually allows you to bake certain algebraic laws into the type.

In contrast, the operational approach does not constrain the semantics of ExitSuccess, there is no associated algebraic law that pertains to every interpreter. It is possible to write interpreters that exit when encountering this instruction, but it is also possible to write interpreters that don't.

Of course, you can prove that any particular interpreter satisfies the law by inspection, for instance because it uses a wildcard pattern match. Sjoerd Visscher observes that you can also enforce this in the type system by changing the return type of ExitSuccess to Void. However, this doesn't work for other laws that can be baked into free monads, for instance the distributive law for the mplus instruction.

Thus, in a confusing turn of events, the operational approach is more free than the free monad, if you interpret "free" as "the least amount of algebraic laws".

It also means that these data types are not isomorphic. However, they are equivalent: every interpreter written with Free can be transformed into an interpreter written with Program and vice versa.

Personally, I like to put all of my laws into the interpreter, because there are a lot of laws that cannot be baked into the free monad, and I like to have them all in one place.

这篇关于运作真的是同构于一个免费的monad吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！