问题描述
我直观地了解MonadFix的纯净，紧缩和嵌套规律。但是，我很难理解滑动定律。
mfix (fmap h . f) = fmap h (mfix (f . h)) -- for strict h
我的第一个问题是，如果h必须严格，那么mfix (f . h)不会是最低值，即⊥？毕竟，f . h直到返回后才必须检查其输入，以免引起悖论。但是，如果h严格，则必须检查其输入。也许我对严格功能的理解是错误的。
第二，为什么这项法律很重要？我能理解纯度，拧紧和套料定律的重要性。但是，我不明白为什么mfix遵守滑动定律很重要。您能否提供一个代码示例来说明为什么滑动定律对MonadFix很重要？
解决方法
我对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。
我无法完全解释法律，但我想我可以提供一些见识。
让我们忘了该方程式的单子函数，让我们假设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)
这与我们想要的法律完全一样。
使用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))
现在，上述推理并不十分严格，但我认为可以在领域理论中将其适当地形式化，即使从数学/理论的角度来看也有意义。
,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的单子都满足。 （因此，将特定案例定为“法律”确实没有意义。）
随着对f (h _|_) = f _|_的较弱要求，我们得到了一个更有用的方程式，该方程式使我们可以处理涉及mfix的项，因为它将其应用于由规则一元函数组成的函数（即{{1} }）和纯字符（即上面的f）。
我们为什么在乎？
您仍然可以问：“我们为什么要关心滑动法则？” @chi的答案提供了直觉。如果您使用单子法绑定法则，则将变得更加清晰。这就是这种表示法的结果：
h如果从左侧看，我们会看到mfix (\x -> f x >>= return . h) = mfix (f . h) >>= return .h
是中央箭头（即，一个仅影响值而不影响“单子”部分的箭头），因此我们期望能够将其“抬起”到return . h的右侧。事实证明，对于任意>>=来说，这个要求实在是太多了：可以证明，许多实际感兴趣的monad并不具有h这样的定义。 （详细信息：请参见Corollary 3.1.7 in Chapter 3。）但是，在许多实际情况下，我们只需要mfix的弱化形式就可以满足。
在图片中，滑动定律使我们可以进行以下转换：
这给了我们直观的认识：我们希望将单子结应用于最小的范围，允许根据需要重新排列/重新排列其他计算。滑动属性会告诉我们确切的时间。