理解 MonadFix 的滑动规律
Understanding the sliding law of MonadFix
我直观地理解了MonadFix的纯度、紧缩和嵌套规律。但是，我很难理解滑动定律。
mfix (fmap h . f) = fmap h (mfix (f . h)) -- for strict h
我的第一个问题是，如果 h 必须严格，那么 mfix (f . h) 会不会是底值，即 ⊥？毕竟，f . h 必须在 returns 之后才检查其输入，这样才不会引起悖论。但是，如果 h 是严格的，那么它将必须检查其输入。也许我对严格函数的理解是错误的。
第二，这部法律为什么重要？我能理解纯度法、收紧法和嵌套法的意义。但是，我不明白为什么 mfix 遵守滑动定律很重要。您能否提供一个代码示例来说明为什么滑动定律对 MonadFix 很重要？
我对 MonadFix 法则一无所知，但我对你问题的第一部分有话要说。 h 严格并不意味着 f . h 也严格。例如取
h = (+ 1) :: Int -> Int
f x = Nothing :: Maybe Int
对于所有输入 x、(f . h) x returns Nothing，因此永远不会调用 h。如果您担心我的 h 没有看起来那么严格，请注意
fmap undefined (mfix (f . undefined)) :: Maybe Int
还有returnsNothing。我选择 h 并不重要，因为根本不会调用 h。
我无法完全解释该定律，但我想我可以提供一些见解。
让我们忘记那个等式的一元部分，让我们假设 f,h :: A -> A 是普通的 non-monadic 函数。然后法律将（非正式地说）简化为以下内容：
fix (h . f) = h (fix (f . h))
这是我discussed in CS.SE前段时间在不动点理论well-known属性
不过，非正式的直觉是 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 的候选人。要在 mfix 之后应用“top-level” h，我们还需要 fmap 它，因为 mfix returns M A。然后我们得到
mfix (fmap h . f) = fmap h (mfix (f . h))
现在，上述推理并不完全严格，但我相信它可以在领域理论中适当地形式化，因此即使从数学/理论的角度来看也是有意义的。
MonadFix 滑动法则
很遗憾，您提供的 link 对滑动定律的描述不正确。它指出：
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 的项，因为它应用于由常规单子函数组成的函数（即 f 以上）和纯的（即上面的 h）。
我们为什么关心？
你还可以问，“我们为什么要关心滑动定律？” @chi 的回答提供了直觉。如果你使用 monadic bind 编写法则，它会变得更加清晰。这是该符号中的结果：
mfix (\x -> f x >>= return . h) = mfix (f . h) >>= return .h
如果你看 left-hand 一侧，我们会看到 return . h 是一个中心箭头（即只影响值而不影响“单子”部分的箭头），因此我们希望能够将其“提升”出 >>= 的 right-hand 一侧。事实证明，这个要求实在是太过分了，for arbitrary h: 可以证明，很多有实际意义的monad都不具备mfix这样的定义。 （详情：参见Corollary 3.1.7 in Chapter 3。）但是我们只需要f (h _|_) = h _|_的弱化形式在许多实际实例中都满足。
在图片中，滑动法可以让我们做如下变换：
这给了我们直觉：我们希望 monadic knot-tying 应用于“最小”可能的范围，允许其他计算 rearranged/shuffled 在必要时进行。滑动 属性 准确告诉我们何时可以。
我直观地理解了MonadFix的纯度、紧缩和嵌套规律。但是，我很难理解滑动定律。
mfix (fmap h . f) = fmap h (mfix (f . h)) -- for strict h
我的第一个问题是，如果 h 必须严格，那么 mfix (f . h) 会不会是底值，即 ⊥？毕竟，f . h 必须在 returns 之后才检查其输入，这样才不会引起悖论。但是，如果 h 是严格的，那么它将必须检查其输入。也许我对严格函数的理解是错误的。
第二，这部法律为什么重要？我能理解纯度法、收紧法和嵌套法的意义。但是，我不明白为什么 mfix 遵守滑动定律很重要。您能否提供一个代码示例来说明为什么滑动定律对 MonadFix 很重要？
我对 MonadFix 法则一无所知，但我对你问题的第一部分有话要说。 h 严格并不意味着 f . h 也严格。例如取
h = (+ 1) :: Int -> Int
f x = Nothing :: Maybe Int
对于所有输入 x、(f . h) x returns Nothing，因此永远不会调用 h。如果您担心我的 h 没有看起来那么严格，请注意
fmap undefined (mfix (f . undefined)) :: Maybe Int
还有returnsNothing。我选择 h 并不重要，因为根本不会调用 h。
我无法完全解释该定律，但我想我可以提供一些见解。
让我们忘记那个等式的一元部分，让我们假设 f,h :: A -> A 是普通的 non-monadic 函数。然后法律将（非正式地说）简化为以下内容：
fix (h . f) = h (fix (f . h))
这是我discussed in CS.SE前段时间在不动点理论well-known属性
不过，非正式的直觉是 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 的候选人。要在 mfix 之后应用“top-level” h，我们还需要 fmap 它，因为 mfix returns M A。然后我们得到
mfix (fmap h . f) = fmap h (mfix (f . h))
现在，上述推理并不完全严格，但我相信它可以在领域理论中适当地形式化，因此即使从数学/理论的角度来看也是有意义的。
MonadFix 滑动法则
很遗憾，您提供的 link 对滑动定律的描述不正确。它指出：
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 的项，因为它应用于由常规单子函数组成的函数（即 f 以上）和纯的（即上面的 h）。
我们为什么关心？
你还可以问，“我们为什么要关心滑动定律？” @chi 的回答提供了直觉。如果你使用 monadic bind 编写法则，它会变得更加清晰。这是该符号中的结果：
mfix (\x -> f x >>= return . h) = mfix (f . h) >>= return .h
如果你看 left-hand 一侧，我们会看到 return . h 是一个中心箭头（即只影响值而不影响“单子”部分的箭头），因此我们希望能够将其“提升”出 >>= 的 right-hand 一侧。事实证明，这个要求实在是太过分了，for arbitrary h: 可以证明，很多有实际意义的monad都不具备mfix这样的定义。 （详情：参见Corollary 3.1.7 in Chapter 3。）但是我们只需要f (h _|_) = h _|_的弱化形式在许多实际实例中都满足。
在图片中，滑动法可以让我们做如下变换：
这给了我们直觉：我们希望 monadic knot-tying 应用于“最小”可能的范围，允许其他计算 rearranged/shuffled 在必要时进行。滑动 属性 准确告诉我们何时可以。