是不是可能不可能完全一样的mfix？

Question

因为Nothing >>= f = Nothing对于每一个f,以下微不足道的定义适用于mfix:

mfix _ = Nothing

但这没有实际用途,因此我们有以下非全面定义:

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

如果这个-clause不会停止,那么mfix f返回会很好.(例如,) 这是不可能的,因为暂停问题无法解决？Nothingletf = Just . (1+)

Answer 1

其中一条MonadFix法则规定,当monadic动作是纯粹的时,monadic fixpoint必须与纯粹的修复点重合:

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.我们可以通过各种方式来近似这个功能,但在这方面最终都达不到完美.