3
4

3 回答 3

5

MonadFix 滑动定律

不幸的是,您提供的链接对滑动定律的描述不正确。它指出:

mfix (fmap h . f) = fmap h (mfix (f . h)) -- for strict h

实际的滑动规律略有不同:

mfix (fmap h . f) = fmap h (mfix (f . h)), when f (h _|_) = f _|_

也就是说,前提条件比要求h严格要弱。它只是问f (h _|_) = f _|_。请注意,如果h是严格的,则自动满足此前提条件。(具体情况见下文。)这种区别在单子情况下很重要,即使相应的法律 forfix没有它:

fix (f . g) = f (fix (g . f)) -- holds without any conditions!

这是因为底层 monad 的绑定通常在其左参数中是严格的,因此可以观察到“移动”的东西。有关详细信息,请参阅单数计算中的值递归第 2.4 节。

严格的h案例

h是严格时,则该定律实际上直接从类型的参数性定理得出(A -> M A) -> M A。这在第 2.6.4 节中确立,特别是在同一文本的推论 2.6.12 中。从某种意义上说,这是“无聊”的情况:也就是说,所有单子都mfix满足它。(因此,将特定案例设为“法律”并没有真正的意义。)

有了较弱的要求,f (h _|_) = f _|_我们得到了一个更有用的方程,它可以让我们操纵涉及的项,mfix因为它应用于由常规单子(即f上面)和纯单子(即上面)组成的函数h

我们为什么关心?

你仍然可以问,“我们为什么要关心滑动定律?” @chi 的回答提供了直觉。如果您使用 monadic bind 编写法律,它会变得更加清晰。这是该符号中的结果:

mfix (\x -> f x >>= return . h) = mfix (f . h) >>= return .h

如果您查看左侧,我们会看到这return . h是一个中心箭头(即,仅影响值但不影响“一元”部分的箭头),因此我们希望能够“提升”它的右侧>>=。事实证明,这个要求太高了,因为任意h:可以证明许多实际感兴趣的单子不具备这样的定义mfix。(细节:见第 3 章推论 3.1.7。)但是我们只需要的弱化形式f (h _|_) = h _|_被许多实际实例满足。

在图片中,滑动定律允许我们进行以下变换:

在此处输入图像描述

这给了我们直觉:我们希望将单子打结应用于“最小”可能的范围,允许其他计算在必要时重新排列/打乱。滑动属性准确地告诉我们何时可能。

于 2020-09-11T15:19:05.567 回答
4

我无法完全解释法律,但我想我可以提供一些见解。

让我们忘记那个方程的单子部分,让我们假设它们f,h :: A -> A是普通的非单子函数。然后,法律将(非正式地)简化为以下内容:

fix (h . f) = h (fix (f . h))

这是我前段时间在 CS.SE 中讨论的不动点理论中的一个众所周知的属性。

然而,非正式的直觉是,最不固定的点g :: A->A是可以写成的东西

fix g = g (g (g (g ....))))

whereg被应用“无限多次”。在这种情况下,什么时候g是这样的组合h . f,我们得到

fix (h . f) = h (f (h (f (h (f ...)))))

同样,

fix (f . h) = f (h (f (h (f (h ...)))))

现在,由于两个应用程序都是无限的,如果我们h在第二个应用程序之上应用,我们希望获得第一个应用程序。在周期数中,4.5(78)它与 相同4.57(87),所以同样的直觉适用。在公式中,

h (fix (f . h)) = fix (h . f)

这正是我们想要的法律。

使用 monad,我们不能像 iff :: A -> M B和那样简单地组合事物h :: B -> A,因为我们需要在fmap这里和那里使用,当然mfix而不是 fix。我们有

fmap h . f :: A -> M A
f . h      :: B -> M B

所以两者都是mfix. 要在之后应用“顶级” hmfix我们还需要fmap它,因为mfix返回M A。然后我们得到

mfix (fmap h . f) = fmap h (mfix (f . h))

现在,上述推理并不完全严格,但我相信它可以在领域理论中适当地形式化,因此即使从数学/理论的角度来看也是有意义的。

于 2020-09-11T12:13:43.530 回答
3

我对 MonadFix 法律一无所知,但我对你问题的第一部分有话要说。h严格并不意味着这f . h也是严格的。例如,取

h = (+ 1) :: Int -> Int
f x = Nothing :: Maybe Int

对于所有输入x(f . h) x返回Nothing,所以h永远不会被调用。如果您担心 myh没有看起来那么严格,请注意

fmap undefined (mfix (f . undefined)) :: Maybe Int

也返回Nothing。我的选择h无关紧要,因为h根本没有被调用。

于 2020-09-11T09:07:44.580 回答