1

如果函数的计算结果为，则for的转换器实现将失败。为什么没有传播过来？MonadFixMaybeTNothingNothingmfix

mfix' :: MonadFix m => (a -> MaybeT m a) -> MaybeT m a
mfix' f = MaybeT $ mfix $ \case
  Nothing -> return Nothing
  Just x -> runMaybeT $ f x

一定有一个很好的理由我没有看到，因为ListT根本没有实现MonadFix，并以与上面相同的方式Maybe实现它。

4

2 回答 2

3

我认为问题只是该error信息具有误导性。我们只关注MonadFix Maybe. 参数mfix可以是四件事之一。

  1. 在输入中可以是严格的：f _|_ = _|_或者“f需要评估它的输入来决定是否返回Nothing或者Just”

    \x -> if x then Nothing else Just True
\x -> x `seq` Nothing
\x -> x `seq` Just x

  2. 可以const Nothing。

  3. 可以Just . f在f不严格的地方。

    Just . (1:)

  4. 它可以是严格的Just . f地方。f

    Just

如果函数是严格的，那么整个事情就会在无限循环中爆炸（就像fix），并且看不到错误，因为我们不知道我们是否会有 aNothing或 a Just。如果是const Nothing，则该函数实际上从未尝试评估error并且什么也没有发生。如果它是Just . f并且f不严格，那么它只是Just $ fix f（根据法律：）mfix $ return . f = return $ fix f。而且，如果f是严格的，我们得到Just _|_（再次，根据法律）。请注意，我们从未看到error触发。

类似的推理适用于MonadFix (MaybeT m). 我认为这次最好举个例子：

runMaybeT $ mfix $ \x -> MaybeT $
             (x `seq` Nothing) :
             Nothing           :
             (Just (1:x))      :
             (Just x)          :
             (x `seq` [])

我上面列出的四个案例中的每一个都在该列表中。结果的第一个元素是无限循环。第二个是Nothing。第三个是repeat 1，第四个是Just无限循环。尝试访问超出此范围的“元素”会触发另一个无限循环，这次是由[]'sMonadFix而不是MaybeT's 引起的。同样，我不相信有可能触发error，因为该函数必须在已经确定结果为 之后强制参数Nothing。

于 2018-04-02T17:05:22.763 回答
2

的定义bomb在引用的库定义中确实非常混乱，尽管函数本身是正确实现的。通过单调性，任何f满足的函数f undefined = Nothing都必须等于const Nothing。因此，定点计算将简单地产生Nothing包裹在变压器堆栈中的正确答案。

有关详细信息，请参阅本作品的第 4.9 节，尽管为清楚起见，原始定义省略了构造函数，并且使用名称ErrT代替MaybeT. （那时 MTL 还不存在！）定义如下：

mfixErrM :: (α → ErrT m α) → ErrT m α
mfixErrM f = mfixM (f · unErr)
     where unErr (Ok a) = a

附录B.7中还有一个证明表明，ErrT m只要底层证券mfixM是m.

于 2018-04-02T20:28:42.043 回答