haskell - 在我们不应该使用monadic bind来使用循环写下mfix的情况下

我一直在尝试使用 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的参数适用于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.

所以，这是我的问题:

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

是具有严格绑定(bind)的单子(monad)，例如Maybe'，
在实践中有趣吗？

是否有示例显示mfix'并非我未找到的完全mfix？

关于IO的小注释:

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

不用担心所有的return和join －它们在这里只是让mfix3和mfix的类型匹配。这个想法是我们将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) -> ...。

最佳答案

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

我们也可以通过使mfix''严格而不是mfix来区分return和(>>=)。

可能不会。 (对“实用”示例的存在的疑问不容易否定地回答。)
在其元素上严格的容器可能就是一个例子。 (如果您想知道官方容器包，它实际上并没有为Monad和Map定义IntMap实例，并且Monad的Seq实例在序列的元素中是惰性的)。
还请注意，尚不清楚单子(monad)法则是否考虑到严格性。如果这样做，那么这些事情就不是合法的monad，因为它们违反了左身身份定律:(return x >>= k) = k x代表x = undefined。

如果您在标准库中使用loop来定义mfix，那么我认为mfix' = mfix，尽管我无法完成证明(我可能错过了一个好窍门，或者缺少了MonadFix法则)。
正如评论中所暗示的那样，争论的重点是严格性。您对mfix'的定义和标准库的loop的定义都小心地将参数函数扩展为懒惰的(分别使用惰性模式(~(_, d))和snd；这两种技术是等效的)。如果恰好放弃了其中的一种预防措施，则mfix和mfix'仍然相等。如果两者均被删除，则存在不匹配(mfix /= mfix')。

关于haskell - 在我们不应该使用monadic bind来使用循环写下mfix的情况下，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/63093464/