理解MonadFix的滑动规律

Question

我直观地理解了MonadFix的纯洁性、紧密性和嵌套规律。然而，我很难理解滑动定律。

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

我的第一个问题是，如果h必须是严格的，那么mfix (f . h)不是最低值吗，即⊥？毕竟，在返回之前，f . h不能检查它的输入，这样它就不会引起悖论。然而，如果h是严格的，那么它将不得不检查它的输入。也许我对严格函数的理解是错误的。

第二，为什么这项法律很重要？我可以理解纯净、紧凑和嵌套法则的意义。然而，我不明白为什么mfix遵循滑动法则是很重要的。您能提供一个代码示例来说明为什么滑动定律对MonadFix很重要吗

Answer 1

我不能完全解释这条法律，但我想我可以提供一些见解。

让我们忘记这个等式的一元部分，让我们假设f,h :: A -> A是简单的、非一元的函数。然后，法律将(非正式地说)简化为以下内容：

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

这是不动点理论中的一个众所周知的性质，我在一段时间以前discussed in CS.SE。

然而，非正式的直觉是，g :: A->A的最小不动点可以写成

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

其中g被应用了“无限多次”。当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)

这和我们想要的规律完全一样。

使用monads，我们不能像使用f :: A -> M B和h :: B -> A那样简单地编写东西，因为我们需要在这里和那里使用fmap，当然还需要使用mfix而不是fix。我们有

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

所以这两个都是mfix的候选者。要在mfix之后应用“顶级”h，我们还需要对其进行fmap，因为mfix返回M A。然后，我们将获得

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

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

Answer 2

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

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

对于所有输入x，(f . h) x返回Nothing，因此永远不会调用h。如果您担心我的h并不像它看起来那么严格，请注意

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

还返回Nothing。我选择的h并不重要，因为h根本不会被调用。

Answer 3

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是严格的，则会自动满足此前提条件。(有关特定情况，请参阅下面的内容。)这种区别在一元情况下很重要，即使fix的相应法律没有这样的区别：

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

这是因为底层monad的绑定通常在其左参数中是严格的，因此可以观察到“移动”的东西。有关详细信息，请参阅Value Recursion in Monadic Computations的第2.4节。

严格的h案例

当h是严格的时，该定律实际上直接从(A -> M A) -> M A类型的参数定理推导而来。这是在Section 2.6.4中建立的，特别是同一文本的推论2.6.12。在某种意义上，这是“无聊”的情况:也就是说，所有具有mfix的monads都满足它。(因此，将特定案例作为“法律”是没有意义的。)

由于f (h _|_) = f _|_的要求较弱，我们得到了一个更有用的方程，它允许我们处理涉及mfix的项，因为它应用于由正则一元函数(即上面的f )和纯函数(即上面的h )组成的函数。

我们为什么要关心呢？

你仍然可以问，“为什么我们关心滑动定律？”@chi的答案提供了直觉。如果你使用一元绑定来编写规则，它就会变得更加清晰。下面是这个符号的结果：

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

如果你看左边，我们看到return . h是一个中心箭头(即，一个只影响值而不是“一元”部分的箭头)，因此我们希望能够将它从>>=的右边“抬起来”。事实证明，对于任意的h，这个要求太高了:可以证明，许多实际感兴趣的monads都没有这样的mfix定义。(详细信息:请参阅Corollary 3.1.7 in Chapter 3。)但是，我们只需要f (h _|_) = h _|_的弱化形式被许多实际实例所满足。

在图片中，滑动定律允许我们进行以下转换：

​

​

这给了我们一种直觉:我们希望将一元打结应用于“最小”的可能范围，允许其他计算在必要时重新排列/打乱。sliding属性确切地告诉我们什么时候可以实现。