6

我一直在尝试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.

所以，这是我的问题：

  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' 类型匹配。这个想法是我们传递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) -> ....

4

1 回答 1

1

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

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

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

具有如此严格绑定的 monad，例如 Maybe'，在实践中是否有趣？

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

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

另请注意，尚不清楚单子定律是否考虑了严格性。如果你这样做了，那么这些东西就不是合法的单子，因为它们违反了左身份定律：(return x >>= k) = k xfor x = undefined.

是否有任何例子表明我没有找到mfix'不完全是？mfix

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

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

于 2020-07-29T19:13:41.907 回答