我们不应该使用 monadic bind 使用 loop 写下 mfix 的情况

Question

我一直在尝试mfix使用Control.Arrow.loop. 我想出了不同的定义，想看看哪个是mfix实际工作中的。

因此，我认为正确的解决方案如下：

mfix' :: MonadFix m => (a -> m a) -> m a
mfix' k = let f ~(_, d) = sequenceA (d, k d)
          in (flip runKleisli () . loop . Kleisli) f

正如人们所见，loop . Kleisli's 论点适用于Applicative实例。我发现这是一个好兆头，因为我们的打结大多被(>>=)正确论证中的严格破坏了。

这是另一个功能。我可以说这不是mfix完全相同的，但我发现的唯一情况不是很自然。看一看：

mfix'' k = let f ~(_, d) = fmap ((,) d) (return d >>= k)
           in (flip runKleisli () . loop . Kleisli) f

据我了解，并非所有严格的右手边绑定都完全强制其论点。例如，在以下情况下IO：

GHCi> mfix'' ((return :: a -> IO a) . (1:))
[1,1,1,1,1,Interrupted.

所以，我决定解决这个问题。我刚刚接受Maybe并强行x进入Just x >>= k：

data Maybe' a = Just' a | Nothing' deriving Show

instance Functor Maybe' where
    fmap = liftM

instance Applicative Maybe' where
    pure  = return
    (<*>) = ap

instance Monad Maybe' where
    return         = Just'
    Nothing' >>= k = Nothing'
    Just' x  >>= k = x `seq` k x

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

有这个在我们手上：

GHCi> mfix ((return :: a -> Maybe' a) . (1:))
[1,1,1,1,1,Interrupted.

GHCi> mfix' ((return :: a -> Maybe' a) . (1:))
[1,1,1,1,1,Interrupted.

GHCi> mfix'' ((return :: a -> Maybe' a) . (1:))
Interrupted.

所以，这里是我的问题：

1. 有没有其他例子可以表明这mfix''不完全mfix？
2. 像这样严格绑定的 monadMaybe'在实践中有趣吗？
3. 是否有任何示例表明这mfix'不完全mfix是我没有找到的？

---

关于 的小注IO：

mfix3 k' = 
    let 
       k = return . k'
       f ~(_, d) = fmap ((,) d) (d >>= k)
    in (join . flip runKleisli () . loop . Kleisli) f

不要担心所有的returns 和joins - 它们在这里只是为了让mfix3's 和mfix's 类型匹配。我们的想法是，我们通过d本身，而不是return d在(>>=)上右手。它为我们提供了以下信息：

GHCi> mfix3 ((return :: a -> IO a) . (1:))
Interrupted.

然而，例如（感谢Li-yao Xia的评论）：

GHCi> mfix3 ((return :: a -> e -> a) . (1:)) ()
[1,1,1,1,1,Interrupted.

---

编辑：感谢HTNW 在评论中对模式匹配的重要说明：最好使用\ ~(_, d) -> ...，而不是\ (_, d) -> ....

Answer 1

这是部分答案，我希望这比没有答案要好。

还有其他例子可以表明 mfix'' 不完全是 mfix 吗？

我们可以通过将strict 代替来mfix''区分。mfixreturn(>>=)

像 Maybe' 这样具有如此严格绑定的 monad 在实践中有趣吗？

可能不会。（关于是否存在“实际”例子的问题不容易得到否定的回答。）

元素严格的容器可能就是一个例子。（如果您想了解官方容器包，它实际上并没有定义和 的Monad实例，并且的实例在序列的元素中是惰性的）。MapIntMapMonadSeq

还要注意的是，尚不清楚单子法则是否考虑了严格性。如果你这样做，那么这些东西就不是合法的单子，因为它们违反了左恒等法则：(return x >>= k) = k x对于x = undefined。

有没有什么例子表明这mfix'不完全mfix是我没有发现的？

loop如果你采用标准库中的定义，mfix那么我认为mfix' = mfix，尽管我无法完成证明（我可能错过了一个好技巧，或者缺少 MonadFix 定律）。

正如评论中所暗示的，争论的要点是严格性。您的定义mfix'和标准库的定义都loop小心地将参数函数扩展为惰性函数（分别使用惰性模式 ( ~(_, d)) 和snd；这两种技术是等效的）。如果仅删除其中一项预防措施，则 和 仍然相等mfix。如果两者均被删除，则mfix'存在不匹配 ( )。mfix /= mfix'