【问题标题】:Understanding the sliding law of MonadFix理解 MonadFix 的滑动规律
【发布时间】:2020-12-29 17:04:44
【问题描述】:

我直观地理解MonadFix 的纯度、紧缩和嵌套法则。但是,我很难理解滑动定律。

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

我的第一个问题是,如果h 必须严格,那么mfix (f . h) 不会是最低值,即?毕竟,f . h 在返回之前不能检查它的输入,以免引起悖论。但是,如果h 是严格的,那么它将必须检查其输入。也许我对严格函数的理解是错误的。

其次,为什么这条法律很重要?我能理解纯洁、紧缩和嵌套法则的重要性。但是,我不明白为什么mfix 遵守滑动定律很重要。您能否提供一个代码示例来说明为什么滑动定律对MonadFix 很重要?

【问题讨论】:

    标签: haskell monads monadfix


    【解决方案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)
    

    这正是我们想要的规律。

    使用 monad,我们不能像 f :: A -> M Bh :: B -> A 那样轻松地组合事物,因为我们需要在这里和那里使用 fmap,当然还有 mfix 而不是修复。我们有

    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))
    

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

    【讨论】:

      【解决方案2】:

      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 的 monad 都满足它。 (因此,将特定案例设为“法律”并没有任何意义。)

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

      我们为什么要关心?

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

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

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

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

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

      【讨论】:

        【解决方案3】:

        我对 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

        【讨论】:

        • 哦,对了。 Haskell 中的评估是由外而内的。因此,f 可以选择是否评估其参数。感谢您澄清这一点。
        猜你喜欢
        • 2014-02-05
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 2016-11-05
        • 2011-01-03
        • 1970-01-01
        • 2023-03-11
        相关资源
        最近更新 更多