haskell - 了解 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))

这是不动点理论中的一个众所周知的性质 I 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)

这正是我们想要的法律。
使用 monad，如果 f :: A -> M B，我们就不能那么容易地组合东西和 h :: B -> A ，因为我们需要使用 fmap这里和那里，当然还有 mfix而不是修复。我们有

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

所以两者都是 mfix 的候选者.申请“顶级” h后 mfix我们还需要 fmap它自 mfix返回 M A .然后我们得到

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

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