haskell - 可能不可能的 mfix 是非平凡的总数吗？

Question

由于Nothing >>= f = Nothing对于 every f，以下简单定义适用于mfix：

mfix _ = Nothing

但这没有实际用途，因此我们有以下非全定义：

mfix f = let a = f (unJust a) in a where
    unJust (Just x) = x
    unJust Nothing = errorWithoutStackTrace "mfix Maybe: Nothing"

如果这个- 子句不会停止，如果mfix f返回就好了。（例如，）这是不可能的，因为停机问题是无法解决的吗？Nothingletf = Just . (1+)

score 8 · Accepted Answer

其中一条MonadFix定律说，当一元动作是纯的时，一元不动点必须与纯不动点重合：

mfix (return . f) = return (fix f)

因此，需要以下内容：

mfix (Just . (1+)) = mfix (return . (1+))
                   = return (fix (1+))
                   = Just (fix (1+))

而且fix (1+)确实是底部。因此，对于您提出的功能，法律明确规定了mfix必须如何表现（并且确实以这种方式表现）。

独立于实例是否符合法律，我们可以询问我们是否喜欢这些法律，或者是否有另一个功能，具有不同的名称和不同的法律，按照您的建议行事；例如，特别是这两个调用的行为应该是这样的：

mfix' (Just . (1+)) = Nothing
mfix' (Just . const 1) = Just 1

由于您所说的原因，这是不可能实现的：停止问题告诉我们，无法确定是否fix f会循环或完成任意f。我们可以通过多种方式来逼近这个函数，但在这方面最终都会达不到完美的效果。

1 回答 1