haskell - 不使用 monadic bind 使用循环写下 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的论点适用于 Applicative实例。我发现这是一个好兆头，因为我们的打结大多被 (>>=) 破坏了。的严格性在正确的论点。
这是另一个功能。我可以看出它不是 mfix完全一样，但我发现的唯一情况不是很自然。看一看:

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

据我了解，并非所有严格的右手绑定(bind)都完全强制其论点。例如，如果是 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 ?

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

有没有例子表明 mfix'不完全是mfix那我有没有发现？

关于 IO 的小注解:

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

不要担心所有 return s 和 join s - 他们来这里只是为了拥有 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) -> ... .

Answer 1

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

Is there any other example which could show that mfix'' is not totally mfix?

我们可以区分 mfix''来自 mfix也可以通过制作 return严格而不是 (>>=) .

Are monads with such a strict bind, like Maybe', interesting in practice?

可能不是。 (关于是否存在“实际”例子的问题不容易否定。)
元素严格的容器可能就是一个例子。 (如果您想知道官方的容器包，它实际上并没有定义 Monad 的 Map 和 IntMap 实例，而 Monad 的 Seq 实例在序列的元素中是惰性的) .
另请注意，尚不清楚单子(monad)定律是否考虑了严格性。如果你这样做了，那么这些东西就不是合法的单子(monad)，因为它们违反了左身份法则: (return x >>= k) = k x对于 x = undefined .

Are there any examples which show that mfix' is not totally mfix that I have not found?

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